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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceAlmostSureConsistency

# Natural-causal almost-sure consistency This module upgrades the heterogeneous natural-causal realized-regret process from `L1` convergence to almost-sure convergence. The proof keeps the same dependent trajectory measure. It applies the first Borel-Cantelli lemma to the summable coordinate model events and to the mass-adapted successor-return events, then consumes the existing fixed-burn-in absolute-regret envelope.

Module map

Declarations
14
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceL1Consistency

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceAlmostSureBehaviorExpectedRegretConsistency

Declarations

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

theorem BanditRLProof.summable_exp_neg_sqrt_natCast Compiled

The stretched-exponential sequence `exp (-sqrt n)` is summable.

theorem summable_exp_neg_sqrt_natCast : Summable (fun n : Nat => Real.exp (-Real.sqrt (n : Real)))
Source line 20 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.natCast_le_successorEpisodeMass Compiled

Positive episode batches make successor mass dominate the round index.

theorem natCast_le_successorEpisodeMass (episodes : Nat -> Nat) (hepisodes : forall t, 0 < episodes t) (rounds : Nat) : (rounds : Real) <= successorEpisodeMass episodes rounds
Source line 83 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.summable_exp_neg_sqrt_successorEpisodeMass Compiled

A mass-adapted `exp (-sqrt mass)` schedule is summable.

theorem summable_exp_neg_sqrt_successorEpisodeMass (episodes : Nat -> Nat) (hepisodes : forall t, 0 < episodes t) : Summable (fun rounds => Real.exp (-Real.sqrt (successorEpisodeMass episodes rounds)))
Source line 96 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.summable_selfConsistentScheduledCausalVanishingReturnDelta Compiled

The natural-causal mass-adapted return failure schedule is summable.

theorem summable_selfConsistentScheduledCausalVanishingReturnDelta (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Summable (selfConsistentScheduledCausalVanishingReturnDelta mdp varianceProxy baseVisitFloor)
Source line 116 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.tsum_selfConsistentScheduledCausalVanishingReturnFailureBudget_ne_top Compiled

The return-failure ENNReal budget is finite.

theorem tsum_selfConsistentScheduledCausalVanishingReturnFailureBudget_ne_top (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : (∑' rounds, ENNReal.ofReal (selfConsistentScheduledCausalVanishingReturnDelta mdp varianceProxy baseVisitFloor rounds)) ≠ ∞
Source line 135 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalVanishingReturnBadEvent Compiled

The actual return-deviation event charged by the summable mass schedule.

noncomputable def selfConsistentScheduledCausalVanishingReturnBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t))
Source line 145 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurableSet_selfConsistentScheduledCausalVanishingReturnBadEvent Compiled

Each event in the summable return schedule is measurable.

theorem measurableSet_selfConsistentScheduledCausalVanishingReturnBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : MeasurableSet (selfConsistentScheduledCausalVanishingReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)
Source line 162 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_trajectoryMeasure_vanishingReturnBadEvent_le Compiled

Every return event is bounded by its mass-adapted failure share.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_vanishingReturnBadEvent_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (rounds : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (selfConsistentScheduledCausalVanishingReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) <= ENNReal.ofReal (selfConsistentScheduledCausalVanishingReturnDelta mdp varianceProxy baseVisitFloor rounds)
Source line 186 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.tsum_selfConsistentScheduledCausalModelRoundBadEvent_measure_ne_top Compiled

The actual coordinate-model event measures have finite total mass.

theorem tsum_selfConsistentScheduledCausalModelRoundBadEvent_measure_ne_top (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (∑' t, source.trajectoryMeasure (selfConsistentScheduledCausalModelRoundBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t)) ≠ ∞
Source line 255 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.tsum_selfConsistentScheduledCausalVanishingReturnBadEvent_measure_ne_top Compiled

The actual return-event measures have finite total mass.

theorem tsum_selfConsistentScheduledCausalVanishingReturnBadEvent_measure_ne_top (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (∑' rounds, source.trajectoryMeasure (selfConsistentScheduledCausalVanishingReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)) ≠ ∞
Source line 278 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.ae_eventually_not_mem_selfConsistentScheduledCausalModel_and_returnBadEvents Compiled

Almost every natural-causal trajectory is eventually model-good and return-good.

theorem ae_eventually_not_mem_selfConsistentScheduledCausalModel_and_returnBadEvents (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor ∀ᵐ trajectory ∂source.trajectoryMeasure, (∀ᶠ t in atTop, trajectory ∉ selfConsistentScheduledCausalModelRoundBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t) ∧ (∀ᶠ rounds in atTop, trajectory ∉ selfConsistentScheduledCausalVanishingReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)
Source line 309 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.ae_eventually_abs_selfConsistentScheduledNaturalCausalRealizedRegret_le_envelope Compiled

Almost every trajectory eventually obeys one fixed-burn-in regret envelope.

theorem ae_eventually_abs_selfConsistentScheduledNaturalCausalRealizedRegret_le_envelope (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor ∀ᵐ trajectory ∂source.trajectoryMeasure, ∃ burnin, ∀ᶠ rounds in atTop, |selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory| <= selfConsistentScheduledCausalBurninRealizedRegretRateEnvelope mdp varianceProxy baseVisitFloor burnin rounds
Source line 356 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_realizedRegret_tendstoAlmostEverywhere_zero Compiled

Natural-causal realized successor-average regret converges almost surely.

theorem selfConsistentScheduledCausalSource_realizedRegret_tendstoAlmostEverywhere_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (forall rounds, Measurable (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)) ∧ ∀ᵐ trajectory ∂source.trajectoryMeasure, Tendsto (fun rounds => selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory) atTop (nhds 0)
Source line 431 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_eventually_modelOptimistic_and_realizedRegret_tendstoAlmostEverywhere_zero Compiled

Almost surely, late empirical models are optimistic while realized regret vanishes.

theorem selfConsistentScheduledCausalSource_eventually_modelOptimistic_and_realizedRegret_tendstoAlmostEverywhere_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : let episodes := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t let rewardBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor t let transitionBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor t let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (forall rounds, Measurable (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)) ∧ ∀ᵐ trajectory ∂source.trajectoryMeasure, (∀ᶠ t in atTop, let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel (episodes t) (mdp.sampledEpisodeBatchOfStochasticTrajectories (episodes t) (trajectory t)) defaultState (rewardBudget t) (transitionBudget t) (forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= model.plan.upperValueRemaining mdp.horizon le_rfl state) ∧ model.plan.optimisticPolicy.expectedRegret initialState <= model.plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * model.plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState) ∧ Tendsto (fun rounds => selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory) atTop (nhds 0)
Source line 492 Chapter context: Finite-horizon RL