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

This module upgrades the actual exploratory source.successorPolicyAt expected-regret process from a.e./in-measure convergence to L1 on the same genuine heterogeneous dependent causal trajectory measure. Every coordinate is measurable, nonnegative, and bounded by the deterministic 2 * horizon policy envelope. Mathlib dominated convergence therefore gives expected absolute convergence directly; no realized-return MGF, independent-window coupling, or extra uniform-integrability assumption is used.

Module map

Declarations
13
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceBehaviorExpectedRegretInMeasureConsistency

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceBehaviorExpectedRegretExplicitIntegratedRate

Declarations

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

theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_le_two_mul_horizon Compiled

The actual successor behavior's expected regret has the global `2H` envelope.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_le_two_mul_horizon

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

theorem selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_le_two_mul_horizon (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (t : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s)) : selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t trajectory <= 2 * (mdp.horizon : Real)
Source line 50 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integrable_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess Compiled

Every behavior expected-regret coordinate is integrable on the causal source.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integrable_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess

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

theorem integrable_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (t : Nat) : Integrable (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t) (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure
Source line 72 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret Compiled

Expected absolute behavior regret at one natural-causal coordinate.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret

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

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

Expected absolute behavior regret converges to zero on the same causal source.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret_tendsto_zero

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

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret_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 (selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0)
Source line 119 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.memLp_one_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess Compiled

Every coordinate of the behavior expected-regret process 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_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess

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

theorem memLp_one_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (t : Nat) : MemLp (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure
Source line 193 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_eq Compiled

The exponent-one extended norm is the lifted expected absolute behavior regret.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_eq

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

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_eq (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (t : Nat) : eLpNorm (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure = ENNReal.ofReal (selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t)
Source line 216 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_tendsto_zero Compiled

The exponent-one extended norm of the behavior 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_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_tendsto_zero

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

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_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 t => eLpNorm (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure) atTop (nhds 0)
Source line 244 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_sub_zero_tendsto_zero Compiled

Canonical exponent-one norm-of-the-difference convergence.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_sub_zero_tendsto_zero

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

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_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 t => eLpNorm (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t - (fun _ => 0)) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure) atTop (nhds 0)
Source line 279 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBehaviorExpectedRegretLp Compiled

The behavior expected-regret process 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.selfConsistentScheduledNaturalCausalBehaviorExpectedRegretLp

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

noncomputable def selfConsistentScheduledNaturalCausalBehaviorExpectedRegretLp (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (t : Nat) : Lp Real 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure
Source line 314 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBehaviorExpectedRegretLp_coeFn_ae_eq Compiled

The named `Lp` coordinate represents the behavior expected-regret process a.e.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBehaviorExpectedRegretLp_coeFn_ae_eq

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

theorem selfConsistentScheduledNaturalCausalBehaviorExpectedRegretLp_coeFn_ae_eq (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (t : Nat) : (selfConsistentScheduledNaturalCausalBehaviorExpectedRegretLp mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor hrewardBound t : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s) -> Real) =ᵐ[ (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure] selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t
Source line 334 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBehaviorExpectedRegretLp_tendsto_zero Compiled

The named behavior expected-regret `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.selfConsistentScheduledNaturalCausalBehaviorExpectedRegretLp_tendsto_zero

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

theorem selfConsistentScheduledNaturalCausalBehaviorExpectedRegretLp_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 (selfConsistentScheduledNaturalCausalBehaviorExpectedRegretLp mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor hrewardBound) atTop (nhds 0)
Source line 361 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_behaviorExpectedRegret_memLp_eLpNorm_L1_tendsto_zero Compiled

Full behavior expected-regret `L1` terminal on the genuine causal source.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_behaviorExpectedRegret_memLp_eLpNorm_L1_tendsto_zero

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

theorem selfConsistentScheduledCausalSource_behaviorExpectedRegret_memLp_eLpNorm_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 (forall t, Integrable (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t) source.trajectoryMeasure) /\ (forall t, MemLp (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t) 1 source.trajectoryMeasure) /\ (forall t, eLpNorm (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t) 1 source.trajectoryMeasure = ENNReal.ofReal (selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t)) /\ Tendsto (selfConsistentScheduledNaturalCausalExpectedAbsoluteBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0) /\ Tendsto (selfConsistentScheduledNaturalCausalBehaviorExpectedRegretLp mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor hrewardBound) atTop (nhds 0) /\ TendstoInMeasure source.trajectoryMeasure (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (fun _ => 0)
Source line 408 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_behaviorExpected_and_realizedRegret_L1_tendsto_zero Compiled

Actual behavior expected and realized regret converge jointly in `L1`.

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

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_behaviorExpected_and_realizedRegret_L1_tendsto_zero

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

theorem selfConsistentScheduledCausalSource_behaviorExpected_and_realizedRegret_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 ((Tendsto (selfConsistentScheduledNaturalCausalBehaviorExpectedRegretLp mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor hrewardBound) atTop (nhds 0)) /\ TendstoInMeasure source.trajectoryMeasure (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (fun _ => 0)) /\ ((Tendsto (selfConsistentScheduledNaturalCausalRealizedRegretLp mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound) atTop (nhds 0)) /\ TendstoInMeasure source.trajectoryMeasure (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (fun _ => 0))
Source line 479 Chapter context: Finite-horizon RL