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.FiniteHorizonNaturalCausalAverageRealizedBehaviorRegretL1Consistency

This module controls the exact natural process which first normalizes every successor batch by its own positive episode count and then weights rounds equally. It is not the total-episode-mass-weighted process from the earlier L1 route. The argument exposes the cumulative normalized-return MGF, obtains a first-moment inverse-square-root bound, and combines it with the compiled logarithmic behavior expected-regret rate.

Module map

Declarations
26
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretInMeasureExplicitSchedule

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalAverageRealizedBehaviorRegretAlmostSureExplicitSchedule, BanditRLProof.RL.FiniteHorizonNaturalCausalBoundedStoppingTimeExplicitExpectedAverageRealizedBehaviorRegret, BanditRLProof.RL.FiniteHorizonNaturalCausalBoundedWindowStoppingTimeL1AverageRealizedBehaviorRegretConsistency

Declarations

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

theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.trajectoryMeasure_naturalCumulativeSuccessorAverageReturnDeviation_hasSubgaussianMGF Compiled

The natural normalized successor-return sum has one global sub-Gaussian MGF.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.trajectoryMeasure_naturalCumulativeSuccessorAverageReturnDeviation_hasSubgaussianMGF

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

theorem trajectoryMeasure_naturalCumulativeSuccessorAverageReturnDeviation_hasSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [forall n, StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, StandardBorelSpace (StochasticEpisodeBatch mdp (episodes n))] [forall n, Nonempty (StochasticEpisodeBatch mdp (episodes n))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) : HasSubgaussianMGF (source.naturalCumulativeSuccessorAverageReturnDeviation rounds) (naturalCumulativeSuccessorAverageReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy) source.trajectoryMeasure
Source line 33 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess_hasSubgaussianMGF Compiled

The self-consistent natural cumulative normalized-return deviation has a global MGF.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess_hasSubgaussianMGF

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

theorem selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess_hasSubgaussianMGF (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) (rounds : Nat) : HasSubgaussianMGF (selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) (selfConsistentScheduledNaturalCausalCumulativeReturnVarianceProxy mdp varianceProxy baseVisitFloor rounds) (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure
Source line 91 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound Compiled

First-moment envelope for the round-normalized cumulative return deviation.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound

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

noncomputable def selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Real
Source line 126 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnInverseSqrtEnvelope Compiled

Coarser inverse-square-root envelope obtained from the linear proxy bound.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnInverseSqrtEnvelope

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

noncomputable def selfConsistentScheduledNaturalCausalAverageReturnInverseSqrtEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (rounds : Nat) : Real
Source line 136 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound_nonneg Compiled

The normalized-return first-moment envelope is nonnegative.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound_nonneg

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

theorem selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : 0 <= selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound mdp varianceProxy baseVisitFloor rounds
Source line 147 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integral_abs_selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess_le Compiled

The MGF controls the absolute first moment of the cumulative return deviation.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integral_abs_selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess_le

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

theorem integral_abs_selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess_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) (rounds : Nat) : integral (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure (fun trajectory => |selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory|) <= 2 * Real.sqrt (selfConsistentScheduledNaturalCausalCumulativeReturnVarianceProxy mdp varianceProxy baseVisitFloor rounds : Real) * Real.exp (1 / 2 : Real)
Source line 156 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound_le_inverseSqrtEnvelope Compiled

The normalized first-moment envelope is bounded by an inverse square root.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound_le_inverseSqrtEnvelope

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

theorem selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound_le_inverseSqrtEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) (hrounds : 0 < rounds) : selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound mdp varianceProxy baseVisitFloor rounds <= selfConsistentScheduledNaturalCausalAverageReturnInverseSqrtEnvelope mdp varianceProxy rounds
Source line 189 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnInverseSqrtEnvelope_tendsto_zero Compiled

The deterministic inverse-square-root return envelope tends to zero.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnInverseSqrtEnvelope_tendsto_zero

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

theorem selfConsistentScheduledNaturalCausalAverageReturnInverseSqrtEnvelope_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) : Tendsto (selfConsistentScheduledNaturalCausalAverageReturnInverseSqrtEnvelope mdp varianceProxy) atTop (nhds 0)
Source line 235 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound_tendsto_zero Compiled

The exact normalized-return first-moment envelope tends to zero on all prefixes.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound_tendsto_zero

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

theorem selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (selfConsistentScheduledNaturalCausalAverageReturnFirstMomentBound mdp varianceProxy baseVisitFloor) atTop (nhds 0)
Source line 251 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integrable_selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess Compiled

The cumulative normalized-return deviation is integrable on every prefix.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integrable_selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess

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

theorem integrable_selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess (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) (rounds : Nat) : Integrable (selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure
Source line 270 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integrable_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess Compiled

The equal-round-weighted natural average realized behavior regret is integrable.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integrable_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess

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

theorem integrable_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess (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) (rounds : Nat) : Integrable (selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure
Source line 292 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret Compiled

Expected absolute equal-round-weighted natural average realized behavior regret.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret

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

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

Deterministic all-prefix L1 envelope for the exact average process.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope

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

noncomputable def selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Real
Source line 356 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope_nonneg Compiled

The deterministic 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.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope_nonneg

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

theorem selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : 0 <= selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope mdp varianceProxy baseVisitFloor rounds
Source line 368 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope_tendsto_zero Compiled

The deterministic all-prefix L1 envelope tends to zero.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope_tendsto_zero

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

theorem selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope mdp varianceProxy baseVisitFloor) atTop (nhds 0)
Source line 383 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret_nonneg Compiled

Expected absolute average realized regret is nonnegative.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret_nonneg

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

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : 0 <= selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds
Source line 397 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret_le_L1Envelope Compiled

The expected absolute exact average process is bounded by the all-prefix L1 envelope.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret_le_L1Envelope

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

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret_le_L1Envelope (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) (rounds : Nat) : selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds <= selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope mdp varianceProxy baseVisitFloor rounds
Source line 411 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret_tendsto_zero Compiled

Expected absolute exact average realized behavior regret tends to zero on all prefixes.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret_tendsto_zero

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

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret_tendsto_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) : Tendsto (selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0)
Source line 537 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.memLp_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess Compiled

Every exact equal-round average realized-regret coordinate belongs to `L1`.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.memLp_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess

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

theorem memLp_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess (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) (rounds : Nat) : MemLp (selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure
Source line 570 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_eq Compiled

At exponent one, `eLpNorm` is the lifted expected absolute exact average regret.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_eq

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

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_eq (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) (rounds : Nat) : eLpNorm (selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure = ENNReal.ofReal (selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)
Source line 595 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_tendsto_zero Compiled

The exponent-one extended norm of the exact average process tends to zero.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_tendsto_zero

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

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_tendsto_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) : Tendsto (fun rounds => eLpNorm (selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure) atTop (nhds 0)
Source line 625 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_sub_zero_tendsto_zero Compiled

The exponent-one norm of the difference from zero tends to zero.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_sub_zero_tendsto_zero

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

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_sub_zero_tendsto_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) : Tendsto (fun rounds => eLpNorm (selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds - (fun _ => 0)) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure) atTop (nhds 0)
Source line 660 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp Compiled

The exact equal-round average realized behavior regret as an `Lp Real 1` value.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp

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

noncomputable def selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp (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) (rounds : Nat) : Lp Real 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure
Source line 695 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp_coeFn_ae_eq Compiled

The named `Lp` coordinate represents the exact average process a.e.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp_coeFn_ae_eq

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

theorem selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp_coeFn_ae_eq (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) (rounds : Nat) : (selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound rounds : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> Real) =ᵐ[ (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure] selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds
Source line 717 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp_tendsto_zero Compiled

The named exact average `Lp Real 1` process converges to zero.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp_tendsto_zero

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

theorem selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp_tendsto_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) : Tendsto (selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound) atTop (nhds 0)
Source line 746 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_naturalAverageRealizedBehaviorRegret_allPrefix_L1_tendsto_zero Compiled

The named exact average `Lp Real 1` process converges to zero. -/ theorem selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp_tendsto_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) : Tendsto (selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound) atTop (nhds 0) := by let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let process := fun rounds => selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds have hmem : forall rounds, MemLp (process rounds) 1 source.trajectoryMeasure := fun rounds => memLp_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound rounds have hzero : MemLp (fun _ : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) => (0 : Real)) 1 source.trajectoryMeasure := MemLp.zero' have hnorm := eLpNorm_one_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_sub_zero_tendsto_zero mdp initialState rewardSource varianceProxy hvarianceProxy law initialTable defaultState support baseVisitFloor hbaseFloor hrewardBound hhorizon hbaseVisitFloor have hLp := (Lp.tendsto_Lp_iff_tendsto_eLpNorm'' process hmem (fun _ => (0 : Real)) hzero).2 (by simpa [process, source] using hnorm) simpa [selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp, process, source] using hLp /- Terminal all-prefix L1 theorem for the exact per-batch-normalized, equal-round-weighted natural realized behavior-regret process.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_naturalAverageRealizedBehaviorRegret_allPrefix_L1_tendsto_zero

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

theorem selfConsistentScheduledCausalSource_naturalAverageRealizedBehaviorRegret_allPrefix_L1_tendsto_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 let process := selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (forall rounds, Integrable (process rounds) source.trajectoryMeasure) /\ (forall rounds, MemLp (process rounds) 1 source.trajectoryMeasure) /\ (forall rounds, selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds <= selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope mdp varianceProxy baseVisitFloor rounds) /\ Tendsto (selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0) /\ (forall rounds, eLpNorm (process rounds) 1 source.trajectoryMeasure = ENNReal.ofReal (selfConsistentScheduledNaturalCausalExpectedAbsoluteAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)) /\ Tendsto (fun rounds => eLpNorm (process rounds - (fun _ => 0)) 1 source.trajectoryMeasure) atTop (nhds 0) /\ Tendsto (selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLp mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound) atTop (nhds 0) /\ TendstoInMeasure source.trajectoryMeasure process atTop (fun _ => 0)
Source line 797 Chapter context: Finite-horizon RL