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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeDecayingExplorationBehaviorConsistency

# Decaying-exploration high-probability behavior consistency This module closes the fixed-exploration residual charge in the exploratory behavior-regret route. It starts from one path-support visit floor at full exploration, proves the exact stagewise power scaling at a smaller exploration rate, and chooses `explorationRate_n = 1 / (n + 2)`, `rounds_n = (n + 2) ^ (horizon + 4)`, and `visitFloor_n = baseVisitFloor * explorationRate_n ^ horizon`. The effective visit mass is therefore `baseVisitFloor * (n + 2) ^ 4`. The scheduled recommendation certificate is `O((n + 2) ^ -2)`, while the behavior exploration charge is `O((n + 2) ^ -1)`. Both the confidence budget and the resulting deterministic average exploratory-behavior expected-regret certificate tend to zero. Each finite window still has its own episode count and trajectory type. The source theorem is consequently a family of finite-window outer-measure certificates, not a pathwise, almost-sure, realized-regret, or common-process convergence theorem.

Module map

Declarations
26
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeExploratoryBehaviorRegret

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeRealizedBehaviorRegret, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardCumulativeDecayingExplorationConsistency

Declarations

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

theorem BanditRLProof.FiniteHorizonRL.exploratoryActionProbabilityFloor_eq_rate_mul_one Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem exploratoryActionProbabilityFloor_eq_rate_mul_one (explorationRate : NNReal) : exploratoryActionProbabilityFloor Action explorationRate = (explorationRate : Real) * exploratoryActionProbabilityFloor Action 1
Source line 45 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.exploratoryPathStateLowerNat_eq_rate_pow_mul_one Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem exploratoryPathStateLowerNat_eq_rate_pow_mul_one {mdp : MDP State Action} {initialState : Measure State} (support : ExploratoryPathSupport mdp initialState) (explorationRate : NNReal) : forall (stage : Nat) (hstage : stage < mdp.horizon) (state : State), exploratoryPathStateLowerNat support explorationRate stage hstage state = (explorationRate : Real) ^ stage * exploratoryPathStateLowerNat support 1 stage hstage state
Source line 54 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.exploratoryPathVisitLower_eq_rate_pow_mul_one Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem exploratoryPathVisitLower_eq_rate_pow_mul_one {mdp : MDP State Action} {initialState : Measure State} (support : ExploratoryPathSupport mdp initialState) (explorationRate : NNReal) (stage : Fin mdp.horizon) (state : State) : exploratoryPathStateLower support explorationRate stage state * exploratoryActionProbabilityFloor Action explorationRate = (explorationRate : Real) ^ (stage.val + 1) * (exploratoryPathStateLower support 1 stage state * exploratoryActionProbabilityFloor Action 1)
Source line 78 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.ExploratoryPathUniformVisitFloor.scale_explorationRate Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem ExploratoryPathUniformVisitFloor.scale_explorationRate {mdp : MDP State Action} {initialState : Measure State} (support : ExploratoryPathSupport mdp initialState) {baseVisitFloor : Real} (hfloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : ExploratoryPathUniformVisitFloor support explorationRate (baseVisitFloor * (explorationRate : Real) ^ mdp.horizon)
Source line 96 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationScale Compiled

No declaration docstring is present; use the chapter context and exact statement below.

def decayingExplorationScale (n : Nat) : Nat
Source line 135 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationRate Compiled

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def decayingExplorationRate (n : Nat) : NNReal
Source line 137 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationRounds Compiled

No declaration docstring is present; use the chapter context and exact statement below.

def decayingExplorationRounds (mdp : MDP State Action) (n : Nat) : Nat
Source line 140 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor Compiled

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def decayingExplorationVisitFloor (mdp : MDP State Action) (baseVisitFloor : Real) (n : Nat) : Real
Source line 143 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes Compiled

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def decayingExplorationScheduledEpisodes (mdp : MDP State Action) (baseVisitFloor : Real) (n : Nat) : Nat
Source line 147 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationAverageRecommendedExpectedRegretBound Compiled

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def decayingExplorationAverageRecommendedExpectedRegretBound (mdp : MDP State Action) (baseVisitFloor : Real) (n : Nat) : Real
Source line 153 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationAverageExploratoryBehaviorExpectedRegretBound Compiled

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def decayingExplorationAverageExploratoryBehaviorExpectedRegretBound (mdp : MDP State Action) (baseVisitFloor : Real) (n : Nat) : Real
Source line 160 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationAverageEnvelope Compiled

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def decayingExplorationAverageEnvelope (mdp : MDP State Action) (baseVisitFloor : Real) (n : Nat) : Real
Source line 165 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationScale_pos Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationScale_pos (n : Nat) : 0 < decayingExplorationScale n
Source line 175 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationRate_pos Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationRate_pos (n : Nat) : 0 < decayingExplorationRate n
Source line 183 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationRate_le_one (n : Nat) : decayingExplorationRate n <= 1
Source line 191 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationRounds_pos Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationRounds_pos (mdp : MDP State Action) (n : Nat) : 0 < decayingExplorationRounds mdp n
Source line 201 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor_pos Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationVisitFloor_pos (mdp : MDP State Action) {baseVisitFloor : Real} (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : 0 < decayingExplorationVisitFloor mdp baseVisitFloor n
Source line 209 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor_mul_rounds Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationVisitFloor_mul_rounds (mdp : MDP State Action) (baseVisitFloor : Real) (n : Nat) : decayingExplorationVisitFloor mdp baseVisitFloor n * (decayingExplorationRounds mdp n : Real) = baseVisitFloor * (decayingExplorationScale n : Real) ^ 4
Source line 220 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationUniformVisitFloor Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationUniformVisitFloor {mdp : MDP State Action} {initialState : Measure State} (support : ExploratoryPathSupport mdp initialState) {baseVisitFloor : Real} (hfloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (n : Nat) : ExploratoryPathUniformVisitFloor support (decayingExplorationRate n) (decayingExplorationVisitFloor mdp baseVisitFloor n)
Source line 251 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.normalizedScheduledAverageEnvelope_decayingExploration_eq Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem normalizedScheduledAverageEnvelope_decayingExploration_eq (mdp : MDP State Action) {baseVisitFloor : Real} (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : normalizedCumulativeInverseSqrtScheduledAverageEnvelope mdp (decayingExplorationRounds mdp n) (decayingExplorationVisitFloor mdp baseVisitFloor n) = decayingExplorationAverageEnvelope mdp baseVisitFloor n
Source line 265 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationAverageEnvelope_tendsto_zero Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationAverageEnvelope_tendsto_zero (mdp : MDP State Action) (baseVisitFloor : Real) : Tendsto (fun n => decayingExplorationAverageEnvelope mdp baseVisitFloor n) atTop (nhds 0)
Source line 295 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationBehaviorCharge_tendsto_zero Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationBehaviorCharge_tendsto_zero (mdp : MDP State Action) : Tendsto (fun n => exploratoryBehaviorRegretCharge mdp (decayingExplorationRate n) 1) atTop (nhds 0)
Source line 315 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationAverageExploratoryBehaviorBound_tendsto_zero Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationAverageExploratoryBehaviorBound_tendsto_zero (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (baseVisitFloor : Real) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (fun n => decayingExplorationAverageExploratoryBehaviorExpectedRegretBound mdp baseVisitFloor n) atTop (nhds 0)
Source line 334 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.decayingExplorationDeltaAndAverageExploratoryBehaviorBound_tendsto_zero Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationDeltaAndAverageExploratoryBehaviorBound_tendsto_zero (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (baseVisitFloor : Real) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (fun n => (ENNReal.ofReal (vanishingAverageConfidenceDelta n), decayingExplorationAverageExploratoryBehaviorExpectedRegretBound mdp baseVisitFloor n)) atTop (nhds (0, 0))
Source line 372 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.decayingExplorationAverageExploratoryBehaviorRegretViolationSet Compiled

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def decayingExplorationAverageExploratoryBehaviorRegretViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (baseVisitFloor : Real) (n : Nat) : Set (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))
Source line 390 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_decayingExplorationAverageExploratoryBehaviorExpectedRegret Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_decayingExplorationAverageExploratoryBehaviorExpectedRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (n : Nat) [StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor 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) : let rounds := AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n let delta := AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n let explorationRate := AdaptiveEpisodeBatchSource.decayingExplorationRate n let visitFloor := AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor mdp baseVisitFloor n let episodes := AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n let countRadius := AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtCountRadius mdp rounds delta visitFloor let source := exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one n) let violationSet := decayingExplorationAverageExploratoryBehaviorRegretViolationSet mdp initialState defaultState baseVisitFloor n MeasurableSet (source.adaptiveCumulativeCountBadEvent rounds delta) /\ source.trajectoryMeasure (source.adaptiveCumulativeCountBadEvent rounds delta) <= ENNReal.ofReal delta /\ violationSet ⊆ source.adaptiveCumulativeCountBadEvent rounds delta /\ source.trajectoryMeasure violationSet <= ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ source.adaptiveCumulativeCountBadEvent rounds delta -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).upperValueRemaining mdp.horizon le_rfl state) /\ adaptiveCumulativeEmpiricalOptimisticAverageExploratoryBehaviorExpectedRegret (initialState
Source line 412 Chapter context: Finite-horizon RL