BanditRLlib

Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeRealizedBehaviorRegret

# Adaptive finite-window realized behavior regret This module transports the compiled adaptive exploratory-policy expected-regret route to realized rewards on the same infinite episode-batch trajectory law. Successor coordinates `1` through `rounds` are charged; coordinate zero is the uncontrolled initial batch and is excluded. Each batch return is centered by the exact history-kernel integral. The bounded-reward contract gives the coarse whole-batch Hoeffding proxy `(episodes * horizon)^2`; this is sufficient for a finite-window realized average certificate, but it is not the sharper within-batch episode proxy. The final decaying-exploration theorem unions the existing cumulative-count bad event with the return-deviation bad event, so its failure budget is two copies of the scheduled confidence level. No common probability space across schedule indices, anytime statement, almost-sure result, or minimax rate is claimed here.

Module map

Source: BanditRLProof/RL/FiniteHorizonAdaptiveCumulativeRealizedBehaviorRegret.lean
Teaching chapter: 9. Finite-horizon reinforcement learning
Declarations: 46
Placeholders: 0

Imports

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeDecayingExplorationBehaviorConsistency

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeDecayingExplorationRealizedBehaviorConsistency

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.FiniteHorizonRL.MDP.traceStateAtFrom Compiled

No declaration docstring is present; use the chapter context and exact statement below.

def traceStateAtFrom (state : State) {n : Nat} (trace : StepTrace Action State n) (stage : Fin n) : State

Source line 37 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.traceStateAtFrom_tail Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem traceStateAtFrom_tail (state : State) {n : Nat} (trace : StepTrace Action State (n + 1)) (stage : Fin n) : traceStateAtFrom (trace 0).2 (Fin.tail trace) stage = traceStateAtFrom state trace stage.succ

Source line 42 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.cumulativeRewardFrom_eq_sum_traceReward Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem cumulativeRewardFrom_eq_sum_traceReward (mdp : MDP State Action) (n : Nat) (state : State) (trace : StepTrace Action State n) : mdp.cumulativeRewardFrom n state trace = ∑ stage : Fin n, mdp.reward (traceStateAtFrom state trace stage) (trace stage).1

Source line 53 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.EpisodeBatch.episodeReturn Compiled

No declaration docstring is present; use the chapter context and exact statement below.

def episodeReturn {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (episode : Fin episodes) : Real

Source line 74 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.EpisodeBatch.totalReturn Compiled

No declaration docstring is present; use the chapter context and exact statement below.

def totalReturn {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) : Real

Source line 78 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.EpisodeBatch.measurable_episodeReturn Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_episodeReturn {mdp : MDP State Action} {episodes : Nat} (episode : Fin episodes) : Measurable (fun batch : EpisodeBatch mdp episodes => episodeReturn batch episode)

Source line 82 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.EpisodeBatch.measurable_totalReturn Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_totalReturn {mdp : MDP State Action} {episodes : Nat} : Measurable (totalReturn : EpisodeBatch mdp episodes -> Real)

Source line 90 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.EpisodeBatch.abs_episodeReturn_le_horizon_of_rewardConsistent Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem abs_episodeReturn_le_horizon_of_rewardConsistent {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (hbatch : batch.RewardConsistent) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (episode : Fin episodes) : |episodeReturn batch episode| <= (mdp.horizon : Real)

Source line 95 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.EpisodeBatch.abs_totalReturn_le_of_rewardConsistent Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem abs_totalReturn_le_of_rewardConsistent {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (hbatch : batch.RewardConsistent) (hrewardBound : forall state action, |mdp.reward state action| <= 1) : |totalReturn batch| <= (episodes : Real) * (mdp.horizon : Real)

Source line 112 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.episodeReturn_episodeBatchOfTrajectories Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem episodeReturn_episodeBatchOfTrajectories (mdp : MDP State Action) (episodes : Nat) (trajectories : Fin episodes -> State × StepTrace Action State mdp.horizon) (episode : Fin episodes) : EpisodeBatch.episodeReturn (mdp.episodeBatchOfTrajectories episodes trajectories) episode = mdp.cumulativeReward (trajectories episode)

Source line 132 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.totalReturn_episodeBatchOfTrajectories Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem totalReturn_episodeBatchOfTrajectories (mdp : MDP State Action) (episodes : Nat) (trajectories : Fin episodes -> State × StepTrace Action State mdp.horizon) : EpisodeBatch.totalReturn (mdp.episodeBatchOfTrajectories episodes trajectories) = ∑ episode : Fin episodes, mdp.cumulativeReward (trajectories episode)

Source line 144 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.batchReturnVarianceProxy Compiled

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def batchReturnVarianceProxy (mdp : MDP State Action) (episodes : Nat) : NNReal

Source line 159 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.integral_cumulativeReward_eval_iidTrajectoryFamilyMeasure Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem integral_cumulativeReward_eval_iidTrajectoryFamilyMeasure {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (episode : Fin episodes) : (∫ trajectories, mdp.cumulativeReward (trajectories episode) ∂policy.iidTrajectoryFamilyMeasure initialState episodes) = ∫ trajectory, mdp.cumulativeReward trajectory ∂policy.trajectoryMeasure initialState

Source line 165 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.integral_totalReturn_iidEpisodeBatchMeasure Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem integral_totalReturn_iidEpisodeBatchMeasure {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : integral (policy.iidEpisodeBatchMeasure initialState episodes) EpisodeBatch.totalReturn = (episodes : Real) * integral (policy.trajectoryMeasure initialState) mdp.cumulativeReward

Source line 183 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.totalReturn_centered_hasSubgaussianMGF Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem totalReturn_centered_hasSubgaussianMGF {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hrewardBound : forall state action, |mdp.reward state action| <= 1) : ProbabilityTheory.HasSubgaussianMGF (fun batch : EpisodeBatch mdp episodes => EpisodeBatch.totalReturn batch - integral (policy.iidEpisodeBatchMeasure initialState episodes) EpisodeBatch.totalReturn) (batchReturnVarianceProxy mdp episodes) (policy.iidEpisodeBatchMeasure initialState episodes)

Source line 210 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.successorReturnKernelMean Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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

Source line 244 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.measurable_successorReturnKernelMean Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_successorReturnKernelMean {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) : Measurable (source.successorReturnKernelMean n)

Source line 251 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.successorReturnKernelMean_eq_selectedPolicy Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem successorReturnKernelMean_eq_selectedPolicy {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) (history : EpisodeBatchPrefix mdp episodes n) : source.successorReturnKernelMean n history = (episodes : Real) * integral ((source.successorPolicy n history).trajectoryMeasure initialState) mdp.cumulativeReward

Source line 258 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.successorReturnPrefixIncrement Compiled

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def successorReturnPrefixIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) : (round : Nat) -> EpisodeBatchPrefix mdp episodes round -> Real | 0, _history => 0 | n + 1, history => EpisodeBatch.totalReturn (history ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩) - source.successorReturnKernelMean n (Preorder.frestrictLe₂ (π

Source line 273 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.measurable_successorReturnPrefixIncrement Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_successorReturnPrefixIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (round : Nat) : Measurable (source.successorReturnPrefixIncrement round)

Source line 287 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.successorReturnIncrement Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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

Source line 307 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.successorReturnIncrement_stronglyAdapted_piLE Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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

Source line 315 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.trajectoryMeasure_condDistrib_totalReturn Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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

Source line 327 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.condExpKernel_map_totalReturn_eq_batchKernel Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem condExpKernel_map_totalReturn_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) : Filter.Eventually (fun trajectory : EpisodeBatchTrajectory mdp episodes => Measure.map (fun path : EpisodeBatchTrajectory mdp episodes => EpisodeBatch.totalReturn (path (n + 1))) (ProbabilityTheory.condExpKernel source.trajectoryMeasure ((inferInstance : MeasurableSpace (EpisodeBatchPrefix mdp episodes n)).comap (Preorder.frestrictLe n)) trajectory) = ((source.batchKernel n).map EpisodeBatch.totalReturn) (Preorder.frestrictLe n trajectory)) (ae (source.trajectoryMeasure.trim (Preorder.measurable_frestrictLe n).comap_le))

Source line 370 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.successorReturnIncrement_succ_hasCondSubgaussianMGF Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem successorReturnIncrement_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) (hrewardBound : forall state action, |mdp.reward state action| <= 1) : ProbabilityTheory.HasCondSubgaussianMGF (Filtration.piLE (X

Source line 409 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.cumulativeSuccessorReturnVarianceProxy Compiled

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def cumulativeSuccessorReturnVarianceProxy (mdp : MDP State Action) (episodes rounds : Nat) : NNReal

Source line 523 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.cumulativeSuccessorReturnDeviation Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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

Source line 530 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.batchReturnVarianceProxy_pos Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem batchReturnVarianceProxy_pos (mdp : MDP State Action) (episodes : Nat) (hepisodes : 0 < episodes) (hhorizon : 0 < mdp.horizon) : 0 < MarkovPolicy.batchReturnVarianceProxy mdp episodes

Source line 537 Chapter context: Finite-horizon RL

theorem

BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.trajectoryMeasure_cumulativeSuccessorReturnDeviation_abs_tail_le

Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem trajectoryMeasure_cumulativeSuccessorReturnDeviation_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) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hhorizon : 0 < mdp.horizon) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : source.trajectoryMeasure {trajectory | Concentration.subGaussianSumConfidenceRadius (cumulativeSuccessorReturnVarianceProxy mdp episodes rounds) delta <= |source.cumulativeSuccessorReturnDeviation rounds trajectory|} <= ENNReal.ofReal delta

Source line 553 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.optimalInitialExpectedReturn Compiled

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def optimalInitialExpectedReturn (mdp : MDP State Action) (initialState : Measure State) : Real

Source line 600 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.successorExpectedCumulativeRegret Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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

Source line 605 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.successorExpectedAverageRegret Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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

Source line 613 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.realizedSuccessorCumulativeRegret Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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

Source line 620 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.realizedSuccessorAverageRegret Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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

Source line 629 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.successorReturnDeviationBadEvent Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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

Source line 637 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.measurable_cumulativeSuccessorReturnDeviation Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_cumulativeSuccessorReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) : Measurable (source.cumulativeSuccessorReturnDeviation rounds)

Source line 648 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.measurableSet_successorReturnDeviationBadEvent Compiled

No declaration docstring is present; use the chapter context and exact statement below.

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

Source line 659 Chapter context: Finite-horizon RL

theorem

BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.successorReturnIncrement_succ_eq_totalReturn_sub_selectedPolicyMean

Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem successorReturnIncrement_succ_eq_totalReturn_sub_selectedPolicyMean {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (trajectory : EpisodeBatchTrajectory mdp episodes) (n : Nat) : source.successorReturnIncrement (n + 1) trajectory = EpisodeBatch.totalReturn (trajectory (n + 1)) - (episodes : Real) * integral ((source.policyAt trajectory (n + 1)).trajectoryMeasure initialState) mdp.cumulativeReward

Source line 668 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.cumulativeSuccessorReturnDeviation_eq_fin_sum Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem cumulativeSuccessorReturnDeviation_eq_fin_sum {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (trajectory : EpisodeBatchTrajectory mdp episodes) (rounds : Nat) : source.cumulativeSuccessorReturnDeviation rounds trajectory = ∑ round : Fin rounds, source.successorReturnIncrement ((round : Nat) + 1) trajectory

Source line 684 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.realizedSuccessorCumulativeRegret_eq_expected_sub_deviation Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem realizedSuccessorCumulativeRegret_eq_expected_sub_deviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (trajectory : EpisodeBatchTrajectory mdp episodes) (rounds : Nat) : source.realizedSuccessorCumulativeRegret trajectory rounds = (episodes : Real) * source.successorExpectedCumulativeRegret trajectory rounds - source.cumulativeSuccessorReturnDeviation rounds trajectory

Source line 701 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.realizedSuccessorAverageRegret_eq_expected_sub_deviation Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem realizedSuccessorAverageRegret_eq_expected_sub_deviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (trajectory : EpisodeBatchTrajectory mdp episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) : source.realizedSuccessorAverageRegret trajectory rounds = source.successorExpectedAverageRegret trajectory rounds - source.cumulativeSuccessorReturnDeviation rounds trajectory / ((episodes : Real) * (rounds : Real))

Source line 733 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.trajectoryMeasure_successorReturnDeviationBadEvent_le Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem trajectoryMeasure_successorReturnDeviationBadEvent_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) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hhorizon : 0 < mdp.horizon) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : source.trajectoryMeasure (source.successorReturnDeviationBadEvent rounds delta) <= ENNReal.ofReal delta

Source line 750 Chapter context: Finite-horizon RL

theorem

BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.trajectoryMeasure_expected_to_realized_successor_average_regret_transport

Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem trajectoryMeasure_expected_to_realized_successor_average_regret_transport {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hhorizon : 0 < mdp.horizon) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (countBadEvent : Set (EpisodeBatchTrajectory mdp episodes)) (expectedBound : Real) (Good : EpisodeBatchTrajectory mdp episodes -> Prop) (hcountMeasurable : MeasurableSet countBadEvent) (hcountTail : source.trajectoryMeasure countBadEvent <= ENNReal.ofReal delta) (hcountGood : forall trajectory, trajectory ∉ countBadEvent -> Good trajectory /\ source.successorExpectedAverageRegret trajectory rounds <= expectedBound) : let returnBadEvent := source.successorReturnDeviationBadEvent rounds delta let combinedBadEvent := countBadEvent ∪ returnBadEvent MeasurableSet combinedBadEvent /\ source.trajectoryMeasure combinedBadEvent <= ENNReal.ofReal delta + ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ combinedBadEvent -> Good trajectory /\ source.realizedSuccessorAverageRegret trajectory rounds <= expectedBound + Concentration.subGaussianSumConfidenceRadius (cumulativeSuccessorReturnVarianceProxy mdp episodes rounds) delta / ((episodes : Real) * (rounds : Real))

Source line 767 Chapter context: Finite-horizon RL

theorem

BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.exploratorySource_successorExpectedCumulativeRegret_eq

Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem exploratorySource_successorExpectedCumulativeRegret_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (trajectory : EpisodeBatchTrajectory mdp episodes) (rounds : Nat) : (exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate).successorExpectedCumulativeRegret trajectory rounds = adaptiveCumulativeEmpiricalOptimisticExploratoryBehaviorExpectedRegret (initialState

Source line 854 Chapter context: Finite-horizon RL

theorem

BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.exploratorySource_successorExpectedAverageRegret_eq

Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem exploratorySource_successorExpectedAverageRegret_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (trajectory : EpisodeBatchTrajectory mdp episodes) (rounds : Nat) : (exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate).successorExpectedAverageRegret trajectory rounds = adaptiveCumulativeEmpiricalOptimisticAverageExploratoryBehaviorExpectedRegret (initialState

Source line 873 Chapter context: Finite-horizon RL

theorem

BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_decayingExplorationAverageRealizedBehaviorRegret

Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_decayingExplorationAverageRealizedBehaviorRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (n : Nat) [StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))] [StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : let rounds := AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n let delta := AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n let explorationRate := AdaptiveEpisodeBatchSource.decayingExplorationRate n let visitFloor := AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor mdp baseVisitFloor n let episodes := AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n let countRadius := AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtCountRadius mdp rounds delta visitFloor let source := exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one n) let countBadEvent := source.adaptiveCumulativeCountBadEvent rounds delta let returnBadEvent := source.successorReturnDeviationBadEvent rounds delta let combinedBadEvent := countBadEvent ∪ returnBadEvent MeasurableSet combinedBadEvent /\ source.trajectoryMeasure combinedBadEvent <= ENNReal.ofReal delta + ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ combinedBadEvent -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).upperValueRemaining mdp.horizon le_rfl state) /\ source.realizedSuccessorAverageRegret trajectory rounds <= AdaptiveEpisodeBatchSource.decayingExplorationAverageExploratoryBehaviorExpectedRegretBound mdp baseVisitFloor n + Concentration.subGaussianSumConfidenceRadius (AdaptiveEpisodeBatchSource.cumulativeSuccessorReturnVarianceProxy mdp episodes rounds) delta / ((episodes : Real) * (rounds : Real))

Source line 890 Chapter context: Finite-horizon RL