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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalAverageRealizedBehaviorRegretAlmostSureConsistency

# All-prefix almost-sure natural causal average realized behavior regret This module strengthens the fourth-power-prefix almost-sure theorem to every deterministic natural prefix for the same per-batch-normalized, equal-round-weighted process on the one heterogeneous causal trajectory measure. The behavior term is the Cesaro average of the compiled almost-everywhere successor-policy expected-regret limit. The return term uses the existing fixed-prefix conditional-sub-Gaussian tail at rounds `n + 1` with summable share `1 / (n + 2)^2`; first Borel-Cantelli needs no event independence. This is not an anytime confidence sequence, stopping-time theorem, raw single-episode process, behavior/recommended-policy equality, minimax rate, reachability theorem, or complete UCB-VI.

Module map

Declarations
21
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonNaturalCausalAverageRealizedBehaviorRegretAlmostSureExplicitSchedule, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceAlmostSureBehaviorExpectedRegretConsistency

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalRandomPrefixAverageRealizedBehaviorRegretAlmostSureConsistency

Declarations

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

def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegretProcess Compiled

Pathwise equal-round average of successor-policy expected regret.

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

Cumulative normalized successor-return deviation divided by round count.

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

Summable confidence share for the return event at prefix `n + 1`.

noncomputable def naturalAllPrefixReturnDelta (n : Nat) : Real
Source line 76 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.naturalAllPrefixReturnDelta_pos Compiled

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

theorem naturalAllPrefixReturnDelta_pos (n : Nat) : 0 < naturalAllPrefixReturnDelta n
Source line 79 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.naturalAllPrefixReturnDelta_le_one Compiled

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

theorem naturalAllPrefixReturnDelta_le_one (n : Nat) : naturalAllPrefixReturnDelta n <= 1
Source line 84 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.summable_naturalAllPrefixReturnDelta Compiled

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

theorem summable_naturalAllPrefixReturnDelta : Summable naturalAllPrefixReturnDelta
Source line 93 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.naturalAllPrefixAverageReturnConfidenceRadius Compiled

Fixed-prefix return radius after division by the positive prefix length.

noncomputable def naturalAllPrefixAverageReturnConfidenceRadius (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : Real
Source line 104 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.naturalAllPrefixAverageReturnConfidenceEnvelope Compiled

Deterministic square-root envelope for the normalized all-prefix radius.

noncomputable def naturalAllPrefixAverageReturnConfidenceEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (n : Nat) : Real
Source line 114 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.log_two_div_naturalAllPrefixReturnDelta_le Compiled

The inverse-square confidence share contributes at most three shifted logs.

theorem log_two_div_naturalAllPrefixReturnDelta_le (n : Nat) : Real.log (2 / naturalAllPrefixReturnDelta n) <= 3 * (1 + Real.log ((n + 2 : Nat) : Real))
Source line 123 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.naturalAllPrefixAverageReturnConfidenceEnvelope_nonneg Compiled

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

theorem naturalAllPrefixAverageReturnConfidenceEnvelope_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (n : Nat) : 0 <= naturalAllPrefixAverageReturnConfidenceEnvelope mdp varianceProxy n
Source line 152 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.naturalAllPrefixAverageReturnConfidenceRadius_le_envelope Compiled

The normalized fixed-prefix return radius is below its deterministic envelope.

theorem naturalAllPrefixAverageReturnConfidenceRadius_le_envelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : naturalAllPrefixAverageReturnConfidenceRadius mdp varianceProxy baseVisitFloor n <= naturalAllPrefixAverageReturnConfidenceEnvelope mdp varianceProxy n
Source line 161 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.naturalAllPrefixAverageReturnConfidenceEnvelope_tendsto_zero Compiled

The deterministic all-prefix return-radius envelope vanishes.

theorem naturalAllPrefixAverageReturnConfidenceEnvelope_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) : Tendsto (naturalAllPrefixAverageReturnConfidenceEnvelope mdp varianceProxy) atTop (nhds 0)
Source line 257 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.naturalAllPrefixAverageReturnConfidenceRadius_tendsto_zero Compiled

The normalized all-prefix return confidence radius vanishes.

theorem naturalAllPrefixAverageReturnConfidenceRadius_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (naturalAllPrefixAverageReturnConfidenceRadius mdp varianceProxy baseVisitFloor) atTop (nhds 0)
Source line 320 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.naturalAllPrefixReturnBadEvent Compiled

Return bad event at positive prefix `n + 1` and inverse-square share.

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

The all-prefix shifted return event is measurable.

theorem measurableSet_naturalAllPrefixReturnBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : MeasurableSet (naturalAllPrefixReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n)
Source line 355 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_trajectoryMeasure_naturalAllPrefixReturnBadEvent_le Compiled

Each shifted return event has probability at most its inverse-square share.

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

The shifted return-event probabilities have finite total mass.

theorem tsum_naturalAllPrefixReturnBadEvent_measure_ne_top (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (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 (∑' n, source.trajectoryMeasure (naturalAllPrefixReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n)) ≠ ∞
Source line 397 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.ae_eventually_not_mem_naturalAllPrefixReturnBadEvent Compiled

Almost every trajectory eventually avoids all shifted return bad events.

theorem ae_eventually_not_mem_naturalAllPrefixReturnBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (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, ∀ᶠ n in atTop, trajectory ∉ naturalAllPrefixReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n
Source line 422 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_naturalAverageBehaviorExpectedRegret_tendstoAlmostEverywhere_zero Compiled

The pathwise behavior expected-regret Cesaro average tends to zero a.e.

theorem selfConsistentScheduledCausalSource_naturalAverageBehaviorExpectedRegret_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 ∀ᵐ trajectory ∂source.trajectoryMeasure, Tendsto (fun rounds => selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory) atTop (nhds 0)
Source line 447 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_naturalAverageReturnDeviation_tendstoAlmostEverywhere_zero Compiled

The equal-round normalized return deviation vanishes on almost every trajectory.

theorem selfConsistentScheduledCausalSource_naturalAverageReturnDeviation_tendstoAlmostEverywhere_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (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, Tendsto (fun rounds => selfConsistentScheduledNaturalCausalAverageReturnDeviationProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory) atTop (nhds 0)
Source line 483 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_naturalAverageRealizedBehaviorRegret_tendstoAlmostEverywhere_zero Compiled

All-prefix natural average realized behavior regret converges almost surely.

theorem selfConsistentScheduledCausalSource_naturalAverageRealizedBehaviorRegret_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 (selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)) ∧ ∀ᵐ trajectory ∂source.trajectoryMeasure, Tendsto (fun rounds => selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory) atTop (nhds 0)
Source line 557 Chapter context: Finite-horizon RL