BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalAverageRealizedBehaviorRegretAlmostSureExplicitSchedule

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.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageBehaviorRegretL1SummableEnvelope

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageReturnL1SummableEnvelope

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretL1SummableEnvelope

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate_explicitRounds_le_summableEnvelope

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound_explicitRounds_le_summableEnvelope

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretL1SummableEnvelope_nonneg

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope_explicitRounds_le_summableEnvelope

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.summable_explicitPolynomialPrefixAverageBehaviorRegretL1SummableEnvelope

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.summable_explicitPolynomialPrefixAverageReturnL1SummableEnvelope

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.summable_explicitPolynomialPrefixAverageRealizedBehaviorRegretL1SummableEnvelope

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret_nonneg

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret_le_summableEnvelope

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.summable_explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixReciprocalThreshold

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixReciprocalThreshold_pos

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability_le_expectedAbsolute_div

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.tsum_explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationProbability_ne_top

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.ae_eventually_not_mem_explicitPolynomialPrefixAverageRealizedBehaviorRegretReciprocalDistanceViolationSet

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.explicitPolynomialPrefixAverageRealizedBehaviorRegret_tendstoAlmostEverywhere_zero

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_explicitPolynomialPrefixAverageRealizedBehaviorRegret_tendstoAlmostEverywhere_zero

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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