Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIAlignment
This module proves, rather than assumes, that each successor batch on the adaptive Kernel.trajMeasure is the literal image of a trajectory generated by the deterministic recurrent policy computed from its strict prefix.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIChargeSummation, BanditRLProof.RL.FiniteHorizonStageVisitFactorization
Imported by
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIProbabilityBudget
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.MDP.measurable_trajectoryStateAt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.MDP.measurable_trajectoryStateAtReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_trajectoryStateAt (mdp : MDP State Action) (stage : Fin mdp.horizon) : Measurable (fun trajectory : State × StepTrace Action State mdp.horizon => mdp.trajectoryStateAt trajectory stage)
theorem
BanditRLProof.FiniteHorizonRL.DeterministicMarkovPolicyTable.trajectoryMeasure_action_eq_table_ae
Compiled
A trajectory generated by a deterministic table records exactly that table's action at every chronological stage, almost surely.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.DeterministicMarkovPolicyTable.trajectoryMeasure_action_eq_table_aeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem trajectoryMeasure_action_eq_table_ae {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : ∀ᵐ trajectory ∂table.toMarkovPolicy.trajectoryMeasure initialState, ∀ stage : Fin mdp.horizon, (mdp.episodeStepOfTrajectory trajectory stage).action = table stage (mdp.trajectoryStateAt trajectory stage)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.iidEpisodeBatchMeasure_successorBatchAligned_ae
Compiled
Under the one-episode mapped batch law, every reconstructed state/action record coincides with the genuine generated trajectory and deterministic table.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.iidEpisodeBatchMeasure_successorBatchAligned_aeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem iidEpisodeBatchMeasure_successorBatchAligned_ae (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (table : DeterministicMarkovPolicyTable mdp) (hhorizon : 0 < mdp.horizon) : ∀ᵐ batch ∂table.toMarkovPolicy.iidEpisodeBatchMeasure initialState 1, let reconstructed : State × StepTrace Action State mdp.horizon := (batch.reconstructedInitialState defaultState, batch.reconstructedStepTrace) ∀ stage : Fin mdp.horizon, (batch 0 stage).state = mdp.trajectoryStateAt reconstructed stage ∧ (batch 0 stage).action = table stage (mdp.trajectoryStateAt reconstructed stage)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_successorBatchAligned_ae
Compiled
Every successor coordinate of the actual recurrent `Kernel.trajMeasure` is aligned with the deterministic table computed from that same trajectory's strict prefix.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_successorBatchAligned_aeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem recurrentSource_trajectoryMeasure_successorBatchAligned_ae (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (n : Nat) : ∀ᵐ trajectory ∂ (recurrentSource mdp initialState defaultState episodes delta).trajectoryMeasure, SuccessorBatchAligned mdp defaultState episodes delta trajectory n
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_all_successorBatchAligned_ae
Compiled
Countable conjunction of the same-source alignment certificates.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_all_successorBatchAligned_aeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem recurrentSource_trajectoryMeasure_all_successorBatchAligned_ae (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) : ∀ᵐ trajectory ∂ (recurrentSource mdp initialState defaultState episodes delta).trajectoryMeasure, ∀ n : Nat, SuccessorBatchAligned mdp defaultState episodes delta trajectory n