Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIAlignment
# Same-source generated-batch alignment for recurrent UCBVI-CH 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.
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.
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.
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.
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.
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