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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeInverseSqrtAverageConsistency

# Scheduled average consistency for adaptive cumulative inverse-square-root recommendations This module chooses an explicit natural number of exploratory episodes per batch. The schedule simultaneously clears the normalized calibration threshold and places the logarithmic factor below one batch's visit mass. The resulting scalar average recommendation-regret bound is at most a fixed constant times `1 / sqrt(rounds)` and therefore tends to zero. The source theorem remains a separate finite-window statement because the episode-batch trajectory type changes with the scheduled batch size.

Module map

Declarations
14
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeInverseSqrtAverageRate

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeInverseSqrtHighProbabilityAverageConsistency

Declarations

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

def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledEpisodeThreshold Compiled

Real-valued batch-size target that clears both normalized calibration and the one-batch logarithmic visit-mass requirement.

noncomputable def normalizedCumulativeInverseSqrtScheduledEpisodeThreshold (mdp : MDP State Action) (rounds : Nat) (delta visitFloor : Real) : Real
Source line 36 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledEpisodes Compiled

Explicit positive natural batch size associated with the scheduled target.

noncomputable def normalizedCumulativeInverseSqrtScheduledEpisodes (mdp : MDP State Action) (rounds : Nat) (delta visitFloor : Real) : Nat
Source line 44 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledAverageEnvelope Compiled

The inverse-square-root envelope for the scheduled average bound.

noncomputable def normalizedCumulativeInverseSqrtScheduledAverageEnvelope (mdp : MDP State Action) (rounds : Nat) (visitFloor : Real) : Real
Source line 53 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.cumulativeInverseSqrtLogFactor_pos Compiled

The valid global confidence budget makes the shared logarithm strict.

theorem cumulativeInverseSqrtLogFactor_pos (mdp : MDP State Action) {rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) {delta : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : 0 < cumulativeInverseSqrtLogFactor mdp rounds delta
Source line 60 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledEpisodeThreshold_nonneg Compiled

The scheduled real-valued target is nonnegative under valid parameters.

theorem normalizedCumulativeInverseSqrtScheduledEpisodeThreshold_nonneg (mdp : MDP State Action) {rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) {delta visitFloor : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) : 0 <= normalizedCumulativeInverseSqrtScheduledEpisodeThreshold mdp rounds delta visitFloor
Source line 77 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledEpisodes_pos Compiled

Every scheduled batch size is positive.

theorem normalizedCumulativeInverseSqrtScheduledEpisodes_pos (mdp : MDP State Action) (rounds : Nat) (delta visitFloor : Real) : 0 < normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor
Source line 96 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledEpisodeThreshold_lt_episodes Compiled

The real-valued target is strictly below the scheduled natural batch size.

theorem normalizedCumulativeInverseSqrtScheduledEpisodeThreshold_lt_episodes (mdp : MDP State Action) (rounds : Nat) (delta visitFloor : Real) : normalizedCumulativeInverseSqrtScheduledEpisodeThreshold mdp rounds delta visitFloor < (normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor : Real)
Source line 108 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtEpisodeThreshold_lt_scheduledEpisodes Compiled

The schedule strictly clears the parent normalized calibration threshold.

theorem normalizedCumulativeInverseSqrtEpisodeThreshold_lt_scheduledEpisodes (mdp : MDP State Action) (rounds : Nat) (delta visitFloor : Real) : normalizedCumulativeInverseSqrtEpisodeThreshold mdp rounds delta visitFloor < (normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor : Real)
Source line 130 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.cumulativeInverseSqrtLogFactor_lt_scheduledEpisodeVisitMass Compiled

One scheduled batch has strictly more visit mass than the log factor.

theorem cumulativeInverseSqrtLogFactor_lt_scheduledEpisodeVisitMass (mdp : MDP State Action) (rounds : Nat) (delta : Real) {visitFloor : Real} (hvisitFloor : 0 < visitFloor) : cumulativeInverseSqrtLogFactor mdp rounds delta < (normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor : Real) * visitFloor / 2
Source line 146 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledAverageBound_nonneg Compiled

The normalized scheduled average bound is nonnegative.

theorem normalizedCumulativeInverseSqrtScheduledAverageBound_nonneg (mdp : MDP State Action) {rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) {delta visitFloor : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) : 0 <= normalizedCumulativeInverseSqrtAverageRecommendedExpectedRegretBound mdp (normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor) rounds delta visitFloor
Source line 163 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledAverageBound_le_envelope Compiled

The scheduled average bound is controlled by a pure inverse-square-root rate.

theorem normalizedCumulativeInverseSqrtScheduledAverageBound_le_envelope (mdp : MDP State Action) {rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) {delta visitFloor : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) : normalizedCumulativeInverseSqrtAverageRecommendedExpectedRegretBound mdp (normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor) rounds delta visitFloor <= normalizedCumulativeInverseSqrtScheduledAverageEnvelope mdp rounds visitFloor
Source line 182 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledAverageEnvelope_tendsto_zero Compiled

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

theorem normalizedCumulativeInverseSqrtScheduledAverageEnvelope_tendsto_zero (mdp : MDP State Action) (visitFloor : Real) : Tendsto (fun n : Nat => normalizedCumulativeInverseSqrtScheduledAverageEnvelope mdp (n + 1) visitFloor) atTop (nhds 0)
Source line 297 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledAverageBound_tendsto_zero Compiled

The scheduled scalar average recommendation-regret bound tends to zero.

theorem normalizedCumulativeInverseSqrtScheduledAverageBound_tendsto_zero (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (delta visitFloor : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) : Tendsto (fun n : Nat => normalizedCumulativeInverseSqrtAverageRecommendedExpectedRegretBound mdp (normalizedCumulativeInverseSqrtScheduledEpisodes mdp (n + 1) delta visitFloor) (n + 1) delta visitFloor) atTop (nhds 0)
Source line 315 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalOptimisticSource.exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_scheduledAverageRecommendedExpectedRegret Compiled

At every positive finite window, the explicit schedule discharges calibration and preserves the parent's measurable event, delta tail, optimism, and average recommended-policy expected-regret conclusion.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_scheduledAverageRecommendedExpectedRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds : Nat) (delta visitFloor : Real) [StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor))] [StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor))] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (support : ExploratoryPathSupport mdp initialState) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) : let episodes := AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor let countRadius := AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtCountRadius mdp rounds delta visitFloor let source := exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate MeasurableSet (source.adaptiveCumulativeCountBadEvent rounds delta) /\ source.trajectoryMeasure (source.adaptiveCumulativeCountBadEvent rounds delta) <= 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) /\ adaptiveCumulativeEmpiricalOptimisticAverageRecommendedExpectedRegret (initialState
Source line 346 Chapter context: Finite-horizon RL