BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeCountMartingaleConfidence

The uncentered real count selected by a visit or transition coordinate.

def rawCount {mdp : MDP State Action} (coordinate : CountCoordinate mdp) {episodes : Nat} (batch : EpisodeBatch mdp episodes) : Real

The iid batch mean of the selected raw count.

noncomputable def policyMean {mdp : MDP State Action} (coordinate : CountCoordinate mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : Real

Every selected raw count is measurable on the batch space.

theorem measurable_rawCount {mdp : MDP State Action} (coordinate : CountCoordinate mdp) {episodes : Nat} : Measurable (coordinate.rawCount : EpisodeBatch mdp episodes -> Real)

The existing coordinate deviation is raw count minus policy mean.

theorem deviation_eq_rawCount_sub_policyMean {mdp : MDP State Action} (coordinate : CountCoordinate mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (batch : EpisodeBatch mdp episodes) : coordinate.deviation policy initialState batch = coordinate.rawCount batch - coordinate.policyMean policy initialState episodes

The kernel integral of a selected raw count is its policy mean.

theorem integral_rawCount_iidEpisodeBatchMeasure {mdp : MDP State Action} (coordinate : CountCoordinate mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : integral (policy.iidEpisodeBatchMeasure initialState episodes) coordinate.rawCount = coordinate.policyMean policy initialState episodes

The selected batch-count deviation has the sharp within-batch Bernoulli proxy.

theorem deviation_hasSubgaussianMGF {mdp : MDP State Action} (coordinate : CountCoordinate mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : ProbabilityTheory.HasSubgaussianMGF (coordinate.deviation policy initialState) (MarkovPolicy.iidBernoulliVarianceProxy episodes) (policy.iidEpisodeBatchMeasure initialState episodes)

Predictable mean of the next selected raw count under the history kernel.

noncomputable def coordinateKernelMean {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) (coordinate : CountCoordinate mdp) (history : EpisodeBatchPrefix mdp episodes n) : Real

The history-kernel raw-count mean is measurable in the finite prefix.

theorem measurable_coordinateKernelMean {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) (coordinate : CountCoordinate mdp) : Measurable (source.coordinateKernelMean n coordinate)

The predictable kernel mean equals the selected-policy iid batch mean.

theorem coordinateKernelMean_eq_policyMean {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) (coordinate : CountCoordinate mdp) (history : EpisodeBatchPrefix mdp episodes n) : source.coordinateKernelMean n coordinate history = coordinate.policyMean (source.successorPolicy n history) initialState episodes

Count increment at a finite prefix. At successor rounds the center is the measurable history-kernel integral, not the potentially nonmeasurable policy selector exposed by the source structure.

noncomputable def coordinatePrefixIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (coordinate : CountCoordinate mdp) : (round : Nat) -> EpisodeBatchPrefix mdp episodes round -> Real | 0, history => coordinate.rawCount (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩) - coordinate.policyMean source.initialPolicy initialState episodes | n + 1, history => coordinate.rawCount (history ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩) - source.coordinateKernelMean n coordinate (Preorder.frestrictLe₂ (π

Every finite-prefix increment is measurable.

theorem measurable_coordinatePrefixIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (coordinate : CountCoordinate mdp) (round : Nat) : Measurable (source.coordinatePrefixIncrement coordinate round)

The adaptive kernel-centered coordinate increment process.

noncomputable def coordinateIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (coordinate : CountCoordinate mdp) (round : Nat) (trajectory : EpisodeBatchTrajectory mdp episodes) : Real

The coordinate increment process is adapted to the canonical prefix filtration.

theorem coordinateIncrement_stronglyAdapted_piLE {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (coordinate : CountCoordinate mdp) : StronglyAdapted (Filtration.piLE (X

The next raw-count conditional distribution is the mapped batch kernel.

theorem trajectoryMeasure_condDistrib_rawCount {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) (coordinate : CountCoordinate mdp) : ProbabilityTheory.condDistrib (fun trajectory : EpisodeBatchTrajectory mdp episodes => coordinate.rawCount (trajectory (n + 1))) (Preorder.frestrictLe n) source.trajectoryMeasure =ᵐ[ source.trajectoryMeasure.map (Preorder.frestrictLe n)] (source.batchKernel n).map coordinate.rawCount

Trimmed conditional-expectation-kernel law for the next adaptive raw count.

theorem condExpKernel_map_rawCount_eq_batchKernel {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) (coordinate : CountCoordinate mdp) : Filter.Eventually (fun trajectory : EpisodeBatchTrajectory mdp episodes => Measure.map (fun path : EpisodeBatchTrajectory mdp episodes => coordinate.rawCount (path (n + 1))) (ProbabilityTheory.condExpKernel source.trajectoryMeasure ((inferInstance : MeasurableSpace (EpisodeBatchPrefix mdp episodes n)).comap (Preorder.frestrictLe n)) trajectory) = ((source.batchKernel n).map coordinate.rawCount) (Preorder.frestrictLe n trajectory)) (ae (source.trajectoryMeasure.trim (Preorder.measurable_frestrictLe n).comap_le))

Initial adaptive batch-count increment has the iid Bernoulli sum proxy.

theorem coordinateIncrement_zero_hasSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (coordinate : CountCoordinate mdp) : ProbabilityTheory.HasSubgaussianMGF (source.coordinateIncrement coordinate 0) (MarkovPolicy.iidBernoulliVarianceProxy episodes) source.trajectoryMeasure

Every successor adaptive count increment is conditionally sub-Gaussian.

theorem coordinateIncrement_succ_hasCondSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) (coordinate : CountCoordinate mdp) : ProbabilityTheory.HasCondSubgaussianMGF (Filtration.piLE (X

Total within-batch variance proxy for a finite adaptive prefix.

noncomputable def cumulativeCoordinateVarianceProxy (episodes rounds : Nat) : NNReal

Delta-calibrated radius for one adaptive cumulative count coordinate.

noncomputable def cumulativeCoordinateConfidenceRadius (episodes rounds : Nat) (delta : Real) : Real

Sum of kernel-centered increments over the first `rounds` batches.

noncomputable def cumulativeCoordinateDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (coordinate : CountCoordinate mdp) (rounds : Nat) (trajectory : EpisodeBatchTrajectory mdp episodes) : Real

Every fixed cumulative coordinate deviation is measurable.

theorem measurable_cumulativeCoordinateDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (coordinate : CountCoordinate mdp) (rounds : Nat) : Measurable (source.cumulativeCoordinateDeviation coordinate rounds)

Two-sided square-root prefix tail for one adaptive cumulative count coordinate.

theorem trajectoryMeasure_cumulativeCoordinateDeviation_abs_tail_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (coordinate : CountCoordinate mdp) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : source.trajectoryMeasure {trajectory | cumulativeCoordinateConfidenceRadius episodes rounds delta <= |source.cumulativeCoordinateDeviation coordinate rounds trajectory|} <= ENNReal.ofReal delta

Equal confidence share for every queried prefix/coordinate pair.

noncomputable def cumulativeCountLocalDelta (mdp : MDP State Action) (rounds : Nat) (delta : Real) : Real

One global bad event covering every cumulative prefix and count coordinate.

noncomputable def adaptiveCumulativeCountBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (delta : Real) : Set (EpisodeBatchTrajectory mdp episodes)

The finite round-coordinate cumulative bad event is measurable.

theorem measurableSet_adaptiveCumulativeCountBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (delta : Real) : MeasurableSet (source.adaptiveCumulativeCountBadEvent rounds delta)

The finite round-coordinate family is nonempty at positive horizon/rounds.

theorem cumulativeCountIndex_nonempty {mdp : MDP State Action} {rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) : Nonempty (Fin rounds × CountCoordinate mdp)

A positive global delta gives a positive local round-coordinate share.

theorem cumulativeCountLocalDelta_pos {mdp : MDP State Action} {rounds : Nat} (hindex : Nonempty (Fin rounds × CountCoordinate mdp)) {delta : Real} (hdelta : 0 < delta) : 0 < cumulativeCountLocalDelta mdp rounds delta

A valid global delta gives every nonempty-family local share at most one.

theorem cumulativeCountLocalDelta_le_one {mdp : MDP State Action} {rounds : Nat} (hindex : Nonempty (Fin rounds × CountCoordinate mdp)) {delta : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : cumulativeCountLocalDelta mdp rounds delta <= 1

The global adaptive cumulative count event has the requested delta budget.

theorem trajectoryMeasure_adaptiveCumulativeCountBadEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : source.trajectoryMeasure (source.adaptiveCumulativeCountBadEvent rounds delta) <= ENNReal.ofReal delta

Outside the union, every queried cumulative deviation is strictly small.

theorem cumulativeCoordinateDeviation_abs_lt_of_not_mem_badEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) {delta : Real} {trajectory : EpisodeBatchTrajectory mdp episodes} (htrajectory : trajectory ∉ source.adaptiveCumulativeCountBadEvent rounds delta) (round : Fin rounds) (coordinate : CountCoordinate mdp) : |source.cumulativeCoordinateDeviation coordinate (round + 1) trajectory| < cumulativeCoordinateConfidenceRadius episodes (round + 1) (cumulativeCountLocalDelta mdp rounds delta)

Predictable center used at one adaptive batch coordinate.

noncomputable def coordinateMeanAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (coordinate : CountCoordinate mdp) : Nat -> EpisodeBatchTrajectory mdp episodes -> Real | 0, _trajectory => coordinate.policyMean source.initialPolicy initialState episodes | n + 1, trajectory => source.coordinateKernelMean n coordinate (Preorder.frestrictLe n trajectory) /-- Sum of predictable coordinate means over a finite prefix. -/ noncomputable def cumulativeCoordinateMean {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (coordinate : CountCoordinate mdp) (rounds : Nat) (trajectory : EpisodeBatchTrajectory mdp episodes) : Real

Sum of predictable coordinate means over a finite prefix.

noncomputable def cumulativeCoordinateMean {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (coordinate : CountCoordinate mdp) (rounds : Nat) (trajectory : EpisodeBatchTrajectory mdp episodes) : Real

Sum of uncentered coordinate counts over a finite prefix.

def cumulativeCoordinateRawCount {mdp : MDP State Action} {episodes : Nat} (coordinate : CountCoordinate mdp) (rounds : Nat) (trajectory : EpisodeBatchTrajectory mdp episodes) : Real

Each adaptive increment is raw count minus its predictable mean.

theorem coordinateIncrement_eq_rawCount_sub_meanAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (coordinate : CountCoordinate mdp) (round : Nat) (trajectory : EpisodeBatchTrajectory mdp episodes) : source.coordinateIncrement coordinate round trajectory = coordinate.rawCount (trajectory round) - source.coordinateMeanAt coordinate round trajectory

The cumulative martingale deviation is raw count minus cumulative mean.

theorem cumulativeCoordinateDeviation_eq_rawCount_sub_mean {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (coordinate : CountCoordinate mdp) (rounds : Nat) (trajectory : EpisodeBatchTrajectory mdp episodes) : source.cumulativeCoordinateDeviation coordinate rounds trajectory = cumulativeCoordinateRawCount coordinate rounds trajectory - source.cumulativeCoordinateMean coordinate rounds trajectory

Cumulative visit raw counts are exactly the summary's visit count.

theorem cumulativeCoordinateRawCount_visit {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) : cumulativeCoordinateRawCount (.visit stage state action) (round + 1) trajectory = ((cumulativeTransitionCountSummaryAt trajectory round).visitCount stage state action : Real)

Cumulative transition raw counts are exactly the summary coordinate.

theorem cumulativeCoordinateRawCount_transition {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : cumulativeCoordinateRawCount (.transition stage state action nextState) (round + 1) trajectory = (cumulativeTransitionCountSummaryAt trajectory round stage state action nextState : Real)

Each transition-count predictable mean factors through its visit mean.

theorem coordinateMeanAt_transition_eq_visit_mul_transition {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (round : Nat) (trajectory : EpisodeBatchTrajectory mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : source.coordinateMeanAt (.transition stage state action nextState) round trajectory = source.coordinateMeanAt (.visit stage state action) round trajectory * (mdp.transition (state, action)).real {nextState}

Cumulative transition centers factor through the cumulative visit center.

theorem cumulativeCoordinateMean_transition_eq_visit_mul_transition {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (trajectory : EpisodeBatchTrajectory mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : source.cumulativeCoordinateMean (.transition stage state action nextState) rounds trajectory = source.cumulativeCoordinateMean (.visit stage state action) rounds trajectory * (mdp.transition (state, action)).real {nextState}

Positive cumulative visits convert the two martingale deviations into a random-denominator empirical-transition singleton bound.

theorem cumulativeEmpiricalTransitionMass_abs_sub_transition_lt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Fin rounds) (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) (radius : Real) (hvisitPos : 0 < (cumulativeTransitionCountSummaryAt trajectory round).visitCount stage state action) (hvisitDeviation : |((cumulativeTransitionCountSummaryAt trajectory round).visitCount stage state action : Real) - source.cumulativeCoordinateMean (.visit stage state action) (round + 1) trajectory| < radius) (htransitionDeviation : |(cumulativeTransitionCountSummaryAt trajectory round stage state action nextState : Real) - source.cumulativeCoordinateMean (.transition stage state action nextState) (round + 1) trajectory| < radius) : |((cumulativeTransitionCountSummaryAt trajectory round).empiricalTransitionKernel defaultState stage (state, action)).real {nextState} - (mdp.transition (state, action)).real {nextState}| < 2 * radius / ((cumulativeTransitionCountSummaryAt trajectory round).visitCount stage state action : Real)

Coordinate radius obtained from the cumulative visit denominator. The zero visit branch uses the trivial probability-mass bound; the positive branch uses the paired visit and transition martingale deviations.

noncomputable def adaptiveCumulativeTransitionCoordinateRadius {mdp : MDP State Action} {episodes rounds : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Fin rounds) (delta : Real) (stage : Fin mdp.horizon) (state : State) (action : Action) (_nextState : State) : Real

Regularity contract connecting the statistical coordinate radius to the planner's count radius after multiplication by the recursive value envelope.

def AdaptiveCumulativeCountMartingaleCover {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (countRadius : TransitionCountRadius) (delta rewardBound : Real) : Prop

Outside the cumulative count-martingale event, the cumulative empirical plan has the finite-coordinate confidence required by the optimistic Bellman route.

noncomputable def coordinateConfidence_of_not_mem_adaptiveCumulativeCountBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) {delta : Real} {trajectory : EpisodeBatchTrajectory mdp episodes} (htrajectory : trajectory ∉ source.adaptiveCumulativeCountBadEvent rounds delta) (round : Fin rounds) (defaultState : State) (countRadius : TransitionCountRadius) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (hcover : forall (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action), (∑ nextState, adaptiveCumulativeTransitionCoordinateRadius trajectory round delta (mdp.decisionStageRemaining remaining hremaining) state action nextState * empiricalFiniteBatchValueEnvelope rewardBound (countRadius.radius 0) remaining) <= countRadius.radius ((cumulativeTransitionCountSummaryAt trajectory round).visitCount (mdp.decisionStageRemaining remaining hremaining) state action)) : (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).CoordinateConfidence where

The cumulative count martingale event and cover produce the reusable global coordinate-confidence contract for cumulative optimistic recommendations.

noncomputable def adaptiveCumulativeCoordinateConfidenceContract_of_martingale {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (defaultState : State) (countRadius : TransitionCountRadius) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hcover : AdaptiveCumulativeCountMartingaleCover (rounds

Generic route endpoint: cumulative count martingales supply the probability producer for optimism and explicit recommended-policy expected regret.

theorem trajectoryMeasure_adaptiveCumulativeCountMartingale_optimism_and_explicitRecommendedExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (defaultState : State) (countRadius : TransitionCountRadius) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hcover : AdaptiveCumulativeCountMartingaleCover (rounds

Concrete exploratory-source endpoint for the cumulative count-martingale confidence route. The conclusion concerns recommended policies, not behavior or realized regret.

theorem exploratorySource_trajectoryMeasure_cumulativeCountMartingale_optimism_and_explicitRecommendedExpectedRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes rounds : Nat) [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hcover : AdaptiveEpisodeBatchSource.AdaptiveCumulativeCountMartingaleCover (rounds