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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeEpisodewiseCommonSpaceL1Consistency

# Common-space L1 realized behavior consistency This module packages the compiled expected absolute realized-regret convergence in Mathlib's native `MemLp`, `eLpNorm`, and `Lp` interfaces. The underlying probability space is still the independent product of complete scheduled finite-window experiments; no nested causal coupling is constructed here.

Module map

Declarations
8
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeEpisodewiseCommonSpaceExpectedConsistency

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardCumulativeDecayingExplorationCommonSpaceL1Consistency

Declarations

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

theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.memLp_one_decayingExplorationEpisodewiseRealizedBehaviorRegretProcess Compiled

Every scheduled common-space realized-regret coordinate belongs to `L1`.

theorem memLp_one_decayingExplorationEpisodewiseRealizedBehaviorRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (n : Nat) : MemLp (decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n) 1 (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor)
Source line 30 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.eLpNorm_one_decayingExplorationEpisodewiseRealizedBehaviorRegretProcess_eq Compiled

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

theorem eLpNorm_one_decayingExplorationEpisodewiseRealizedBehaviorRegretProcess_eq (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (n : Nat) : eLpNorm (decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n) 1 (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor) = ENNReal.ofReal (decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegret mdp initialState initialTable defaultState baseVisitFloor n)
Source line 48 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.eLpNorm_one_decayingExplorationEpisodewiseRealizedBehaviorRegretProcess_tendsto_zero Compiled

The exponent-one extended `Lp` norm of the scheduled process tends to zero.

theorem eLpNorm_one_decayingExplorationEpisodewiseRealizedBehaviorRegretProcess_tendsto_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (hbatchBorel : forall n, StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (htrajectoryBorel : forall n, StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (fun n => eLpNorm (decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n) 1 (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor)) atTop (nhds 0)
Source line 71 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.eLpNorm_one_decayingExplorationEpisodewiseRealizedBehaviorRegretProcess_sub_zero_tendsto_zero Compiled

Canonical `L1` convergence form: the norm of the difference from zero tends to zero.

theorem eLpNorm_one_decayingExplorationEpisodewiseRealizedBehaviorRegretProcess_sub_zero_tendsto_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (hbatchBorel : forall n, StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (htrajectoryBorel : forall n, StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (fun n => eLpNorm (decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n - (fun _ => 0)) 1 (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor)) atTop (nhds 0)
Source line 108 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.decayingExplorationEpisodewiseRealizedBehaviorRegretLp Compiled

The scheduled realized-regret process represented as an `Lp Real 1` value.

noncomputable def decayingExplorationEpisodewiseRealizedBehaviorRegretLp (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (n : Nat) : Lp Real 1 (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor)
Source line 145 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.decayingExplorationEpisodewiseRealizedBehaviorRegretLp_coeFn_ae_eq Compiled

The named `Lp` coordinate represents the original process almost everywhere.

theorem decayingExplorationEpisodewiseRealizedBehaviorRegretLp_coeFn_ae_eq (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (n : Nat) : (decayingExplorationEpisodewiseRealizedBehaviorRegretLp mdp initialState initialTable defaultState baseVisitFloor hrewardBound n : DecayingExplorationEpisodewiseWindowSpace mdp baseVisitFloor -> Real) =ᵐ[ decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor] decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n
Source line 161 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.decayingExplorationEpisodewiseRealizedBehaviorRegretLp_tendsto_zero Compiled

The named `Lp Real 1` scheduled process converges to zero in the `Lp` topology.

theorem decayingExplorationEpisodewiseRealizedBehaviorRegretLp_tendsto_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (hbatchBorel : forall n, StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (htrajectoryBorel : forall n, StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (decayingExplorationEpisodewiseRealizedBehaviorRegretLp mdp initialState initialTable defaultState baseVisitFloor hrewardBound) atTop (nhds 0)
Source line 179 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.exploratorySource_decayingExplorationEpisodewiseCommonMeasure_memLp_eLpNorm_L1_tendsto_zero Compiled

Terminal `L1` theorem: coordinate membership, exact norms, canonical norm convergence, convergence in the `Lp` topology, and the induced convergence in measure all hold on the same common probability space.

theorem exploratorySource_decayingExplorationEpisodewiseCommonMeasure_memLp_eLpNorm_L1_tendsto_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (hbatchBorel : forall n, StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (htrajectoryBorel : forall n, StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : (forall n, MemLp (decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n) 1 (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor)) /\ (forall n, eLpNorm (decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n) 1 (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor) = ENNReal.ofReal (decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegret mdp initialState initialTable defaultState baseVisitFloor n)) /\ Tendsto (fun n => eLpNorm (decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n - (fun _ => 0)) 1 (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor)) atTop (nhds 0) /\ Tendsto (decayingExplorationEpisodewiseRealizedBehaviorRegretLp mdp initialState initialTable defaultState baseVisitFloor hrewardBound) atTop (nhds 0) /\ TendstoInMeasure (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor) (decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor) atTop (fun _ => 0)
Source line 226 Chapter context: Finite-horizon RL