Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalSource
# Heterogeneous causal source for the actual-sampled self-consistent schedule The compiled self-consistent finite-window theorems vary the batch size and algorithm parameters with the outer window index. Their laws therefore are not prefixes of one fixed adaptive source. This module defines the distinct causal algorithm in which those parameters vary at each trajectory coordinate. The coordinate type itself is dependent: coordinate `n` contains a stochastic episode batch of size `episodes n`. Mathlib's dependent `Kernel.trajMeasure` then constructs one Ionescu-Tulcea law. The terminal theorem records the exact initial law, every selected next-batch conditional law, the prefix/next `compProd` factorization, and projective consistency of all finite marginals. Local APIs/imports are the actual-sampled measurable optimistic table, `exploratoryIIDStochasticEpisodeBatchKernel`, dependent `Kernel.trajMeasure`, `Kernel.condDistrib_trajMeasure`, `map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure`, and measurable finite restrictions. Retrieval found no existing heterogeneous actual-sampled causal-source route; `KernelTrajectoryPrefix.trajMeasure_map_frestrictLe_congr` is supporting local evidence. Regularity for the law construction is finite measurable nonempty State and Action with equality and measurable singletons plus a probability initial law. Standard Borel State/Action is needed only for the `condDistrib` endpoint. Failure policy: this is a new round-varying algorithm. It preserves actual sampled rewards and uses only the latest completed batch, but it does not have the old fixed-window laws as marginals and does not inherit their confidence, optimism, regret, or rate theorem. Those require new heterogeneous concentration and regret transports. No pathwise, almost-sure, anytime, minimax, reachability, or complete-UCB-VI claim is made here.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentExplicitRate, BanditRLProof.KernelTrajectoryPrefix
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalModelConfidence, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalReturnConcentration
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
abbrev
BanditRLProof.FiniteHorizonRL.HeterogeneousStochasticEpisodeBatchTrajectory
Compiled
A trajectory whose complete stochastic batch size may vary by coordinate.
abbrev HeterogeneousStochasticEpisodeBatchTrajectory (mdp : MDP State Action) (episodes : Nat -> Nat)
abbrev
BanditRLProof.FiniteHorizonRL.HeterogeneousStochasticEpisodeBatchPrefix
Compiled
A finite dependent batch history through coordinate `n`.
abbrev HeterogeneousStochasticEpisodeBatchPrefix (mdp : MDP State Action) (episodes : Nat -> Nat) (n : Nat)
structure
BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource
Compiled
An adaptive source of stochastic episode batches with coordinate-dependent batch sizes.
structure HeterogeneousAdaptiveStochasticEpisodeBatchSource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat -> Nat) where
def
BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.trajectoryMeasure
Compiled
The one-process dependent Ionescu-Tulcea trajectory law.
noncomputable def trajectoryMeasure {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : Measure (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)
theorem
BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.trajectoryMeasure_map_eval_zero
Compiled
Coordinate zero has the configured initial stochastic batch law.
theorem trajectoryMeasure_map_eval_zero {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : source.trajectoryMeasure.map (Function.eval 0) = source.rewardSource.iidStochasticTrajectoryFamilyMeasure source.initialPolicy initialState (episodes 0)
theorem
BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.trajectoryMeasure_prefix_compProd
Compiled
Every prefix/next marginal has the configured causal `compProd` law.
theorem trajectoryMeasure_prefix_compProd {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) : source.trajectoryMeasure.map (Preorder.frestrictLe n) ⊗ₘ source.batchKernel n = source.trajectoryMeasure.map (fun trajectory => (Preorder.frestrictLe n trajectory, trajectory (n + 1)))
theorem
BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.trajectoryMeasure_condDistrib_nextBatch
Compiled
The regular conditional law of coordinate `n + 1` is its source kernel.
theorem trajectoryMeasure_condDistrib_nextBatch {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) [StandardBorelSpace (StochasticEpisodeBatch mdp (episodes (n + 1)))] [Nonempty (StochasticEpisodeBatch mdp (episodes (n + 1)))] : condDistrib (fun trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes => trajectory (n + 1)) (Preorder.frestrictLe n) source.trajectoryMeasure =ᵐ[ source.trajectoryMeasure.map (Preorder.frestrictLe n)] source.batchKernel n
theorem
BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.trajectoryMeasure_map_prefix_projective
Compiled
Finite marginals of the causal law form a projective family.
theorem trajectoryMeasure_map_prefix_projective {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) {m n : Nat} (hmn : m <= n) : (source.trajectoryMeasure.map (Preorder.frestrictLe n)).map (Preorder.frestrictLe₂ (π
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.heterogeneousLatestBatch
Compiled
The latest batch in a dependent finite history.
def heterogeneousLatestBatch {mdp : MDP State Action} {episodes : Nat -> Nat} {n : Nat} (history : HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n) : StochasticEpisodeBatch mdp (episodes n)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_heterogeneousLatestBatch
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_heterogeneousLatestBatch {mdp : MDP State Action} {episodes : Nat -> Nat} {n : Nat} : Measurable (heterogeneousLatestBatch : HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n -> StochasticEpisodeBatch mdp (episodes n))
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.heterogeneousSuccessorTable
Compiled
The actual-sampled optimistic table selected from dependent history.
noncomputable def heterogeneousSuccessorTable {mdp : MDP State Action} {episodes : Nat -> Nat} (defaultState : State) (rewardBudget transitionBudget : Nat -> Real) (n : Nat) (history : HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n) : DeterministicMarkovPolicyTable mdp
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_heterogeneousSuccessorTable
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_heterogeneousSuccessorTable {mdp : MDP State Action} {episodes : Nat -> Nat} (defaultState : State) (rewardBudget transitionBudget : Nat -> Real) (n : Nat) : Measurable (heterogeneousSuccessorTable (mdp
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.heterogeneousExploratorySource
Compiled
Actual-sampled exploratory source with coordinate-dependent batch sizes, budgets, and exploration rates.
noncomputable def heterogeneousExploratorySource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat -> Nat) (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBudget transitionBudget : Nat -> Real) (explorationRate : Nat -> NNReal) (hexplorationRate : forall n, explorationRate n <= 1) : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes where
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource
Compiled
The genuinely causal round-varying self-consistent scheduled source.
noncomputable def selfConsistentScheduledCausalSource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState (fun n => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_trajectoryMeasure_exactLaws_and_projective
Compiled
Exact conditional and projective laws of the self-consistent causal source.
theorem selfConsistentScheduledCausalSource_trajectoryMeasure_exactLaws_and_projective (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) : let episodes := fun n => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure.map (Function.eval 0) = rewardSource.iidStochasticTrajectoryFamilyMeasure (initialTable.exploratoryPolicy (AdaptiveEpisodeBatchSource.decayingExplorationRate 0) (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one 0)) initialState (episodes 0) /\ (forall n history, source.batchKernel n history = rewardSource.iidStochasticTrajectoryFamilyMeasure ((heterogeneousSuccessorTable defaultState (fun k => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor k) (fun k => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor k) n history).exploratoryPolicy (AdaptiveEpisodeBatchSource.decayingExplorationRate (n + 1)) (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one (n + 1))) initialState (episodes (n + 1))) /\ (forall n, condDistrib (fun trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes => trajectory (n + 1)) (Preorder.frestrictLe n) source.trajectoryMeasure =ᵐ[ source.trajectoryMeasure.map (Preorder.frestrictLe n)] source.batchKernel n) /\ (forall n, source.trajectoryMeasure.map (Preorder.frestrictLe n) ⊗ₘ source.batchKernel n = source.trajectoryMeasure.map (fun trajectory => (Preorder.frestrictLe n trajectory, trajectory (n + 1)))) /\ (forall m n (hmn : m <= n), (source.trajectoryMeasure.map (Preorder.frestrictLe n)).map (Preorder.frestrictLe₂ (π