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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentExplicitRate

# Explicit finite-window rate for sampled self-consistent optimism This consumer keeps the scheduled source and all its regularity contracts unchanged. It combines the compiled bounds `rewardBudget < scale^-2`, `q < 4 * card State * horizon / scale^2`, and `q <= 1 / 2` to expose closed finite-window failure and realized-regret envelopes. The proof route uses only the local self-consistent schedule, the explicit exploration charge, the normalized return-radius envelope, and ordered-field algebra (`MLIB-ORDER-ALGEBRA`, `MLIB-REAL-LOG-SQRT`, and `MLIB-ASYMPTOTICS`). No theorem-card or proof-weapon statement is used as a Lean proof. Failure policy: preserve actual sampled rewards, three separate confidence shares, global return centering, and changing finite-window sample spaces. A failure here must remain a rate-algebra or local-API issue; it must not be repaired by weakening the source law, replacing sampled rewards by means, or claiming a common process, anytime control, minimax regret, or complete UCB-VI.

Module map

Declarations
14
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentSchedule

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalExplicitRate, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalSource, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCommonSpaceConsistency

Declarations

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

def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudgetRateEnvelope Compiled

Three times the compiled contraction envelope controls the fixed-point budget.

noncomputable def selfConsistentScheduledTransitionBudgetRateEnvelope (mdp : MDP State Action) (n : Nat) : Real
Source line 44 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudgetRateEnvelope_eq Compiled

The explicit transition-budget envelope is `12 * |State| * horizon / scale^2`.

theorem selfConsistentScheduledTransitionBudgetRateEnvelope_eq (mdp : MDP State Action) (n : Nat) : selfConsistentScheduledTransitionBudgetRateEnvelope mdp n = (12 * (Fintype.card State : Real) * (mdp.horizon : Real)) / (AdaptiveEpisodeBatchSource.decayingExplorationScale n : Real) ^ 2
Source line 52 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget_le_rateEnvelope Compiled

The exact fixed-point transition budget has an explicit scale-squared rate.

theorem selfConsistentScheduledTransitionBudget_le_rateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor n <= selfConsistentScheduledTransitionBudgetRateEnvelope mdp n
Source line 62 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledPlanningAverageRegretRateEnvelope Compiled

Explicit planning envelope: scale-squared model error plus the exploration charge.

noncomputable def selfConsistentScheduledPlanningAverageRegretRateEnvelope (mdp : MDP State Action) (n : Nat) : Real
Source line 127 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledPlanningAverageRegretBound_le_rateEnvelope Compiled

The scheduled planning certificate is bounded by the explicit rate envelope.

theorem selfConsistentScheduledPlanningAverageRegretBound_le_rateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : selfConsistentScheduledPlanningAverageRegretBound mdp varianceProxy baseVisitFloor n <= selfConsistentScheduledPlanningAverageRegretRateEnvelope mdp n
Source line 137 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope Compiled

Closed full realized-rate envelope, including the global return fluctuation.

noncomputable def selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (n : Nat) : Real
Source line 171 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedSuccessorAverageRegretBound_le_rateEnvelope Compiled

The original realized-regret certificate is bounded by the closed rate envelope.

theorem selfConsistentScheduledRealizedSuccessorAverageRegretBound_le_rateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : selfConsistentScheduledRealizedSuccessorAverageRegretBound mdp varianceProxy baseVisitFloor n <= selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy n
Source line 177 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedFailureRateEnvelope Compiled

The three confidence shares equal the explicit `3 / (n + 2)` envelope.

noncomputable def selfConsistentScheduledRealizedFailureRateEnvelope (n : Nat) : ENNReal
Source line 196 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedFailureBudget_eq_rateEnvelope Compiled

The old three-share budget is exactly the explicit failure-rate envelope.

theorem selfConsistentScheduledRealizedFailureBudget_eq_rateEnvelope (n : Nat) : selfConsistentScheduledRealizedFailureBudget n = selfConsistentScheduledRealizedFailureRateEnvelope n
Source line 207 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledPlanningAverageRegretRateEnvelope_tendsto_zero Compiled

The explicit planning-rate envelope tends to zero.

theorem selfConsistentScheduledPlanningAverageRegretRateEnvelope_tendsto_zero (mdp : MDP State Action) : Tendsto (selfConsistentScheduledPlanningAverageRegretRateEnvelope mdp) atTop (nhds 0)
Source line 226 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope_tendsto_zero Compiled

The full explicit realized-regret envelope tends to zero.

theorem selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) : Tendsto (selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy) atTop (nhds 0)
Source line 257 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedFailureRateEnvelope_tendsto_zero Compiled

The explicit `3 / (n + 2)` failure envelope tends to zero.

theorem selfConsistentScheduledRealizedFailureRateEnvelope_tendsto_zero : Tendsto selfConsistentScheduledRealizedFailureRateEnvelope atTop (nhds 0)
Source line 275 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledExplicitRateEnvelopes_tendsto_zero Compiled

Explicit failure and realized-regret rates vanish jointly.

theorem selfConsistentScheduledExplicitRateEnvelopes_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) : Tendsto (fun n => (selfConsistentScheduledRealizedFailureRateEnvelope n, selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy n)) atTop (nhds (0, 0))
Source line 288 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.exploratorySource_trajectoryMeasure_selfConsistentScheduledExplicitRate_allCoordinateConfidence_optimism_and_realizedSuccessorAverageRegret Compiled

Actual-sampled optimism and realized regret with explicit finite-window rates.

theorem exploratorySource_trajectoryMeasure_selfConsistentScheduledExplicitRate_allCoordinateConfidence_optimism_and_realizedSuccessorAverageRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (n : Nat) (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (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 episodes := AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n let rewardBudget := AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor n let transitionBudget := AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor n let source := exploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one n) let modelBadEvent := source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy delta delta let returnBadEvent := source.successorGlobalReturnDeviationBadEvent rounds 1 varianceProxy delta let combinedBadEvent := modelBadEvent ∪ returnBadEvent MeasurableSet combinedBadEvent /\ source.trajectoryMeasure combinedBadEvent <= AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedFailureRateEnvelope n /\ forall trajectory, trajectory ∉ combinedBadEvent -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveStochasticSampledEmpiricalOptimisticPlanAt trajectory defaultState rewardBudget transitionBudget round).upperValueRemaining mdp.horizon le_rfl state) /\ source.realizedSuccessorAverageRegret trajectory rounds <= AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy n
Source line 312 Chapter context: Finite-horizon RL