Lean module · EXP3
BanditRLProof.Exp3BernsteinAllHorizon
# All-horizon realized EXP3 Bernstein route The explicit Bernstein schedule gives its `11 * gamma * T` threshold when the three large-horizon inequalities make clipping inactive. This module closes the complementary branch honestly: generated realized losses are at most one almost surely, comparator predictable losses are nonnegative pointwise, and therefore realized regret is at most `T` almost surely. A branch threshold uses `T + 1` outside the Bernstein regime, yielding one theorem for every positive horizon without pretending that the clipped branch satisfies cubic dominance.
Module map
Imports
BanditRLProof.Exp3BernsteinExplicitTuning
Imported by
BanditRLProof, BanditRLProof.Exp3MixedSquareBernsteinRealizedAllHorizon, BanditRLProof.Exp3MixedSquareExponentialRealizedAllHorizon, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedDoublePathwiseVarianceProbabilisticSparsityAllHorizon, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovAllHorizon, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovProbabilisticSparsityAllHorizon, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsityAllHorizon, BanditRLProof.Exp3RandomSquareBernsteinRealizedAllHorizon
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Exp3.predictableLossAt_nonneg
Compiled
Every predictable comparator coordinate is nonnegative.
theorem predictableLossAt_nonneg {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (loss : PredictableLossVector Env Action) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) (action : Action) : 0 <= predictableLossAt loss t sample action
theorem
BanditRLProof.Exp3.sampledPredictableTrajectoryMeasure_realizedLoss_le_one_ae
Compiled
Each generated realized scalar loss is at most one almost surely.
theorem sampledPredictableTrajectoryMeasure_realizedLoss_le_one_ae {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (t : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment ∀ᵐ sample ∂mu, sampledTrajectoryRealizedLossAt t sample <= 1
theorem
BanditRLProof.Exp3.sampledPredictableTrajectoryMeasure_finiteHorizon_realizedLoss_le_one_ae
Compiled
One common almost-sure event bounds every realized scalar loss strictly before a finite horizon.
theorem sampledPredictableTrajectoryMeasure_finiteHorizon_realizedLoss_le_one_ae {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (horizon : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment ∀ᵐ sample ∂mu, ∀ t, t < horizon -> sampledTrajectoryRealizedLossAt t sample <= 1
theorem
BanditRLProof.Exp3.sampledPredictable_realizedRegret_le_horizon_ae
Compiled
Generated selected-loss regret against any comparator is at most the horizon almost surely.
theorem sampledPredictable_realizedRegret_le_horizon_ae {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (comparator : Action) (horizon : Nat) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment ∀ᵐ sample ∂mu, (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator) <= (horizon : Real)
theorem
BanditRLProof.Exp3.sampledPredictable_trivialRealizedRegret_tail
Compiled
The strict `T + 1` threshold has zero failure probability under the generated trajectory law.
theorem sampledPredictable_trivialRealizedRegret_tail {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_nonneg : 0 <= gamma) (hgamma_le_one : gamma <= 1) (loss : PredictableLossVector Env Action) (comparator : Action) (horizon : Nat) (delta : Real) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_nonneg hgamma_le_one loss.environment mu {sample | (horizon : Real) + 1 <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta
def
BanditRLProof.Exp3.bernsteinLargeHorizonCondition
Compiled
The regime in which the clipped explicit schedule satisfies the Bernstein dominance contracts without activating its clip.
def bernsteinLargeHorizonCondition (K T delta : Real) : Prop
def
BanditRLProof.Exp3.bernsteinAllHorizonRegretThreshold
Compiled
All-horizon threshold: use the explicit Bernstein rate in its valid regime and the strict pathwise horizon fallback otherwise.
noncomputable def bernsteinAllHorizonRegretThreshold (K T delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_allHorizonBernsteinRealizedRegret_tail
Compiled
Generated realized-regret tail for every positive horizon. In the explicit large-horizon regime the threshold is `11 * gamma * T`; otherwise the theorem uses the genuine almost-sure `T` regret bound and threshold `T + 1`.
theorem sampledPredictable_allHorizonBernsteinRealizedRegret_tail {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (hcard_two : 2 <= arms.card) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let gamma := bernsteinClippedExplorationRate (arms.card : Real) (horizon : Real) delta let eta := bernsteinHighProbabilityLearningRate (arms.card : Real) (horizon : Real) gamma let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (bernsteinClippedExplorationRate_pos (arms.card : Real) (horizon : Real) delta (by exact_mod_cast hcard_two) (by exact_mod_cast hhorizon)).le (by exact (bernsteinClippedExplorationRate_le_half (arms.card : Real) (horizon : Real) delta).trans (by norm_num)) loss.environment mu {sample | bernsteinAllHorizonRegretThreshold (arms.card : Real) (horizon : Real) delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta