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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceL1Consistency

# Natural causal L1 consistency for heterogeneous scheduled batches This route strengthens the compiled convergence-in-probability theorem on the single heterogeneous causal trajectory measure. It does not use the independent product of complete finite-window experiments. The expected selected-policy regret is uniformly bounded by `2 * horizon`. After a fixed burn-in, the compiled model certificate controls its good-event part, while the summable model tail pays the bounded bad-event contribution. The globally centered sampled-return deviation is integrated directly from its conditional sub-Gaussian MGF and divided by the actual successor episode mass. Regularity is unchanged: finite nonempty Standard Borel State/Action spaces, a probability initial law, positive horizon/base visit floor/reward proxy, bounded stored means, a uniform mean-compatible selected-reward sub-Gaussian law, and the existing full-exploration path floor. Failure policy: preserve the one dependent causal source, actual coordinate batch sizes, `n`-prefix to `n + 1` policy selection, successor-only initial exclusion, global centering, and actual-mass normalization. No pathwise, almost-sure, anytime, minimax, state-reachability, or complete UCB-VI statement is inferred.

Module map

Declarations
27
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceConsistency

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceAlmostSureConsistency

Declarations

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

theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorWeightedExpectedAverageRegret_le_two_mul_horizon Compiled

Every heterogeneous weighted selected-policy average is at most `2H`.

theorem successorWeightedExpectedAverageRegret_le_two_mul_horizon {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) (hmass : 0 < successorEpisodeMass episodes rounds) (hrewardBound : forall state action, |mdp.reward state action| <= 1) : source.successorWeightedExpectedAverageRegret trajectory rounds <= 2 * (mdp.horizon : Real)
Source line 45 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.trajectoryMeasure_cumulativeSuccessorGlobalReturnDeviation_hasSubgaussianMGF Compiled

The heterogeneous successor deviation has one global sub-Gaussian MGF.

theorem trajectoryMeasure_cumulativeSuccessorGlobalReturnDeviation_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.cumulativeSuccessorGlobalReturnDeviation rounds) (cumulativeSuccessorGlobalReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy) source.trajectoryMeasure
Source line 94 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.integrable_realizedSuccessorAverageRegret Compiled

Finite-prefix heterogeneous realized successor-average regret is integrable.

theorem integrable_realizedSuccessorAverageRegret {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) (hrounds : 0 < rounds) (hepisodes : forall t, 0 < episodes t) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (hrewardBoundOne : forall state action, |mdp.reward state action| <= 1) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) : Integrable (source.realizedSuccessorAverageRegret (rounds
Source line 149 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.normalizedSuccessorGlobalReturnMGFFirstMomentBound Compiled

Direct first-moment envelope for the normalized heterogeneous deviation.

noncomputable def normalizedSuccessorGlobalReturnMGFFirstMomentBound (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) : Real
Source line 216 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.normalizedSuccessorGlobalReturnMGFFirstMomentBound_nonneg Compiled

The normalized heterogeneous MGF first-moment envelope is nonnegative.

theorem normalizedSuccessorGlobalReturnMGFFirstMomentBound_nonneg (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) : 0 <= normalizedSuccessorGlobalReturnMGFFirstMomentBound mdp episodes rounds rewardBound rewardVarianceProxy
Source line 230 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.normalizedSuccessorGlobalReturnMGFFirstMomentBound_le_confidenceRadius Compiled

A sufficiently wide normalized confidence radius dominates the MGF mean.

theorem normalizedSuccessorGlobalReturnMGFFirstMomentBound_le_confidenceRadius (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (delta : Real) (hmass : 0 < successorEpisodeMass episodes rounds) (hlog : (1 / 2 : Real) <= Real.log (2 / delta)) : normalizedSuccessorGlobalReturnMGFFirstMomentBound mdp episodes rounds rewardBound rewardVarianceProxy <= 2 * Real.exp (1 / 2 : Real) * normalizedSuccessorGlobalReturnConfidenceRadius mdp episodes rounds rewardBound rewardVarianceProxy delta
Source line 244 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalTailModelFailureBudget_ne_top Compiled

Every post-burn-in model budget is finite.

theorem selfConsistentScheduledCausalTailModelFailureBudget_ne_top (mdp : MDP State Action) (burnin : Nat) : selfConsistentScheduledCausalTailModelFailureBudget mdp burnin ≠ ⊤
Source line 298 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalTailModelFailureBudget_toReal_tendsto_zero Compiled

The real-valued post-burn-in model tail also tends to zero.

theorem selfConsistentScheduledCausalTailModelFailureBudget_toReal_tendsto_zero (mdp : MDP State Action) : Tendsto (fun burnin => (selfConsistentScheduledCausalTailModelFailureBudget mdp burnin).toReal) atTop (nhds 0)
Source line 317 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalNormalizedReturnMGFFirstMomentBound Compiled

Scheduled direct-MGF contribution under actual successor mass.

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

The scheduled direct-MGF contribution is nonnegative.

theorem selfConsistentScheduledCausalNormalizedReturnMGFFirstMomentBound_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : 0 <= selfConsistentScheduledCausalNormalizedReturnMGFFirstMomentBound mdp varianceProxy baseVisitFloor rounds
Source line 341 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalNormalizedReturnMGFFirstMomentBound_tendsto_zero Compiled

The scheduled direct-MGF first-moment contribution tends to zero.

theorem selfConsistentScheduledCausalNormalizedReturnMGFFirstMomentBound_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (selfConsistentScheduledCausalNormalizedReturnMGFFirstMomentBound mdp varianceProxy baseVisitFloor) atTop (nhds 0)
Source line 353 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalBurninExpectedRegretRateEnvelope_nonneg Compiled

The fixed-burn-in expected-regret envelope is nonnegative.

theorem selfConsistentScheduledCausalBurninExpectedRegretRateEnvelope_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) : 0 <= selfConsistentScheduledCausalBurninExpectedRegretRateEnvelope mdp varianceProxy baseVisitFloor burnin rounds
Source line 421 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret Compiled

Expected absolute regret of one natural causal prefix.

noncomputable def selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret (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 452 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalBurninExpectedAbsoluteRegretL1Envelope Compiled

Two-parameter direct `L1` envelope after a fixed model burn-in.

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

The direct natural-causal `L1` envelope is nonnegative.

theorem selfConsistentScheduledCausalBurninExpectedAbsoluteRegretL1Envelope_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) : 0 <= selfConsistentScheduledCausalBurninExpectedAbsoluteRegretL1Envelope mdp varianceProxy baseVisitFloor burnin rounds
Source line 481 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integrable_selfConsistentScheduledNaturalCausalRealizedRegretProcess Compiled

Every coordinate of the natural causal realized-regret process is integrable.

theorem integrable_selfConsistentScheduledNaturalCausalRealizedRegretProcess (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 (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure
Source line 496 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret_nonneg Compiled

Expected absolute natural-causal regret is nonnegative.

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret_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 <= selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds
Source line 547 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret_le_burninL1Envelope Compiled

The expected absolute natural-causal regret is controlled by the good-event planning envelope, the bounded model-tail overflow, and the directly integrated global-return MGF contribution.

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret_le_burninL1Envelope (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) (burnin rounds : Nat) (hburnin : burnin <= rounds) (hrounds : 0 < rounds) : selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds <= selfConsistentScheduledCausalBurninExpectedAbsoluteRegretL1Envelope mdp varianceProxy baseVisitFloor burnin rounds
Source line 566 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret_tendsto_zero Compiled

Expected absolute regret on the natural causal prefixes tends to zero.

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

Every coordinate of the natural causal process belongs to `L1`.

theorem memLp_one_selfConsistentScheduledNaturalCausalRealizedRegretProcess (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 (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure
Source line 860 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalRealizedRegretProcess_eq Compiled

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

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalRealizedRegretProcess_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 (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure = ENNReal.ofReal (selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)
Source line 884 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalRealizedRegretProcess_tendsto_zero Compiled

The exponent-one extended norm on the causal prefixes tends to zero.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalRealizedRegretProcess_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 (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure) atTop (nhds 0)
Source line 914 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalRealizedRegretProcess_sub_zero_tendsto_zero Compiled

Canonical natural-causal `L1` norm-of-the-difference convergence.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalRealizedRegretProcess_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 (selfConsistentScheduledNaturalCausalRealizedRegretProcess 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 949 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalRealizedRegretLp Compiled

The natural causal realized-regret process as an `Lp Real 1` value.

noncomputable def selfConsistentScheduledNaturalCausalRealizedRegretLp (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 984 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalRealizedRegretLp_coeFn_ae_eq Compiled

The named natural-causal `Lp` coordinate represents the process a.e.

theorem selfConsistentScheduledNaturalCausalRealizedRegretLp_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) : (selfConsistentScheduledNaturalCausalRealizedRegretLp 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] selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds
Source line 1005 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalRealizedRegretLp_tendsto_zero Compiled

The named natural-causal `Lp Real 1` process converges to zero.

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

Terminal natural-causal `L1` theorem on one heterogeneous dependent trajectory measure: exact exponent-one norms, `Lp` convergence, and convergence in measure.

theorem selfConsistentScheduledCausalSource_naturalRealizedRegret_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 rounds, MemLp (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 1 source.trajectoryMeasure) /\ (forall rounds, eLpNorm (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) 1 source.trajectoryMeasure = ENNReal.ofReal (selfConsistentScheduledNaturalCausalExpectedAbsoluteRealizedRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)) /\ Tendsto (fun rounds => eLpNorm (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds - (fun _ => 0)) 1 source.trajectoryMeasure) atTop (nhds 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 1084 Chapter context: Finite-horizon RL