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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalAverageRealizedBehaviorRegretAlmostSureExplicitSchedule

# Explicit-schedule almost-sure consistency for natural average realized behavior regret This module keeps the exact process which divides every successor batch by its own positive episode count and then weights rounds equally. Along the deterministic fourth-power prefixes `(n + 1)^4`, its compiled all-prefix L1 envelope is dominated by a sum of shifted exponent-three and exponent-two p-series. Markov's inequality and the first Borel-Cantelli lemma then give almost-everywhere convergence on this subsequence. This is not the older total-episode-mass-weighted process and is not an all-prefix, anytime, or stopping-time almost-sure result.

Module map

Declarations
21
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonNaturalCausalAverageRealizedBehaviorRegretL1Consistency

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalAverageRealizedBehaviorRegretAlmostSureConsistency, BanditRLProof.RL.FiniteHorizonNaturalCausalGrowingWindowGridStoppingTimeL1AverageRealizedBehaviorRegretConsistency, BanditRLProof.RL.FiniteHorizonNaturalCausalPolynomialBaseGrowingRawWindowStoppingTimeL1AverageRealizedBehaviorRegretConsistency, BanditRLProof.RL.FiniteHorizonNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageVanishingDelayProbabilityAndL1Consistency

Declarations

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

def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageBehaviorRegretL1SummableEnvelope Compiled

Shifted exponent-three envelope for the scheduled behavior-regret L1 term.

noncomputable def explicitPolynomialPrefixAverageBehaviorRegretL1SummableEnvelope (mdp : MDP State Action) (n : Nat) : Real
Source line 36 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageReturnL1SummableEnvelope Compiled

Shifted exponent-two envelope for the scheduled normalized-return L1 term.

noncomputable def explicitPolynomialPrefixAverageReturnL1SummableEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (n : Nat) : Real
Source line 42 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretL1SummableEnvelope Compiled

Summable deterministic L1 envelope on the fourth-power prefix schedule.

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

The scheduled logarithmic average is dominated by a shifted exponent-three term.

theorem selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate_explicitRounds_le_summableEnvelope (mdp : MDP State Action) (n : Nat) : selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate mdp (explicitHighProbabilityRounds n) <= explicitPolynomialPrefixAverageBehaviorRegretL1SummableEnvelope mdp n
Source line 59 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound_explicitRounds_le_summableEnvelope Compiled

The scheduled return first moment is dominated by a shifted exponent-two term.

theorem selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound_explicitRounds_le_summableEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound mdp varianceProxy baseVisitFloor (explicitHighProbabilityRounds n) <= explicitPolynomialPrefixAverageReturnL1SummableEnvelope mdp varianceProxy n
Source line 99 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretL1SummableEnvelope_nonneg Compiled

The explicit scheduled L1 envelope is nonnegative.

theorem explicitPolynomialPrefixAverageRealizedBehaviorRegretL1SummableEnvelope_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (n : Nat) : 0 <= explicitPolynomialPrefixAverageRealizedBehaviorRegretL1SummableEnvelope mdp varianceProxy n
Source line 131 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope_explicitRounds_le_summableEnvelope Compiled

The all-prefix L1 envelope is pointwise controlled on fourth-power prefixes.

theorem selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope_explicitRounds_le_summableEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope mdp varianceProxy baseVisitFloor (explicitHighProbabilityRounds n) <= explicitPolynomialPrefixAverageRealizedBehaviorRegretL1SummableEnvelope mdp varianceProxy n
Source line 150 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.summable_explicitPolynomialPrefixAverageBehaviorRegretL1SummableEnvelope Compiled

The shifted exponent-three behavior envelope is summable.

theorem summable_explicitPolynomialPrefixAverageBehaviorRegretL1SummableEnvelope (mdp : MDP State Action) : Summable (explicitPolynomialPrefixAverageBehaviorRegretL1SummableEnvelope mdp)
Source line 169 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.summable_explicitPolynomialPrefixAverageReturnL1SummableEnvelope Compiled

The shifted exponent-two return envelope is summable.

theorem summable_explicitPolynomialPrefixAverageReturnL1SummableEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) : Summable (explicitPolynomialPrefixAverageReturnL1SummableEnvelope mdp varianceProxy)
Source line 188 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.summable_explicitPolynomialPrefixAverageRealizedBehaviorRegretL1SummableEnvelope Compiled

The deterministic fourth-power scheduled L1 envelope is summable.

theorem summable_explicitPolynomialPrefixAverageRealizedBehaviorRegretL1SummableEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) : Summable (explicitPolynomialPrefixAverageRealizedBehaviorRegretL1SummableEnvelope mdp varianceProxy)
Source line 211 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret Compiled

Expected absolute exact average realized regret on the fourth-power schedule.

noncomputable def explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : Real
Source line 224 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret_nonneg Compiled

The scheduled expected absolute process is nonnegative.

theorem explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : 0 <= explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n
Source line 237 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret_le_summableEnvelope Compiled

The scheduled expected absolute process is bounded by the summable envelope.

theorem explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret_le_summableEnvelope (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) (n : Nat) : explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n <= explicitPolynomialPrefixAverageRealizedBehaviorRegretL1SummableEnvelope mdp varianceProxy n
Source line 253 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.summable_explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret Compiled

Scheduled expected absolute exact average realized regret is summable.

theorem summable_explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret (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) : Summable (explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor)
Source line 282 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixReciprocalThreshold Compiled

Reciprocal thresholds used to turn fixed-threshold Borel-Cantelli into convergence.

noncomputable def explicitPolynomialPrefixReciprocalThreshold (k : Nat) : Real
Source line 314 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixReciprocalThreshold_pos Compiled

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

theorem explicitPolynomialPrefixReciprocalThreshold_pos (k : Nat) : 0 < explicitPolynomialPrefixReciprocalThreshold k
Source line 317 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability_le_expectedAbsolute_div Compiled

Markov's inequality for one scheduled distance-from-zero violation.

theorem explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability_le_expectedAbsolute_div (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 epsilon : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hepsilon : 0 < epsilon) (n : Nat) : explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n <= ENNReal.ofReal (explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n / epsilon)
Source line 323 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.tsum_explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability_ne_top Compiled

Fixed positive scheduled violation probabilities have finite total mass.

theorem tsum_explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability_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) (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) (epsilon : Real) (hepsilon : 0 < epsilon) : (∑' n, explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n) ≠ ∞
Source line 399 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.ae_eventually_not_mem_explicitPolynomialPrefixAverageRealizedBehaviorRegretReciprocalDistanceViolationSet Compiled

Almost every trajectory eventually avoids every reciprocal scheduled violation.

theorem ae_eventually_not_mem_explicitPolynomialPrefixAverageRealizedBehaviorRegretReciprocalDistanceViolationSet (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, forall k, ∀ᶠ n in atTop, trajectory ∉ explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (explicitPolynomialPrefixReciprocalThreshold k) n
Source line 435 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegret_tendstoAlmostEverywhere_zero Compiled

The exact equal-round average process converges a.e. on fourth-power prefixes.

theorem explicitPolynomialPrefixAverageRealizedBehaviorRegret_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 n => explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n trajectory) atTop (nhds 0)
Source line 470 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_explicitPolynomialPrefixAverageRealizedBehaviorRegret_tendstoAlmostEverywhere_zero Compiled

Scheduled L1 summability and almost-sure consistency on the common source.

theorem selfConsistentScheduledCausalSource_explicitPolynomialPrefixAverageRealizedBehaviorRegret_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 n, Measurable (explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n)) ∧ Summable (explicitPolynomialPrefixAverageRealizedBehaviorRegretL1SummableEnvelope mdp varianceProxy) ∧ Summable (explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) ∧ (forall epsilon, 0 < epsilon -> (∑' n, explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon n) ≠ ∞) ∧ ∀ᵐ trajectory ∂source.trajectoryMeasure, Tendsto (fun n => explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n trajectory) atTop (nhds 0)
Source line 523 Chapter context: Finite-horizon RL