Lean module · EXP3
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovAESparsityAllHorizon
This module replaces the universal pathwise sparse-support contract of the existing all-horizon route by an almost-everywhere contract under the exact generated trajectory measure. The large-horizon branch combines the compiled raw sparse-loss tail with the tuned and explicit budget comparisons. The complementary branch keeps the strict T + 1 zero-probability fallback.
Module map
Imports
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovAllHorizon
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Exp3.sampledPredictable_allHorizonSparseLossPredictableVarianceRealizedMarkovRegret_tail_of_ae_sparsity
Compiled
Generated sparse-loss realized-regret tail for every positive horizon when support sparsity holds almost everywhere under the exact internally tuned trajectory measure.
Used in these reading views: Bandit Book · Online Learning Book
7. EXP3 and adversarial concentration
Canonical node identity
declaration:BanditRLProof.Exp3.sampledPredictable_allHorizonSparseLossPredictableVarianceRealizedMarkovRegret_tail_of_ae_sparsityReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sampledPredictable_allHorizonSparseLossPredictableVarianceRealizedMarkovRegret_tail_of_ae_sparsity {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 sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let gamma := sparseLossPredictableVarianceClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) delta let eta := sparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (sparseLossPredictableVarianceClippedExplorationRate_pos (arms.card : Real) (sparsity : Real) (horizon : Real) delta (by exact_mod_cast hcard_two) (by exact_mod_cast hsparsity) (by exact_mod_cast hhorizon)).le (by exact (sparseLossPredictableVarianceClippedExplorationRate_le_half (arms.card : Real) (sparsity : Real) (horizon : Real) delta).trans (by norm_num)) loss.environment (∀ᵐ sample ∂mu, ∀ t, t < horizon → (sampledPredictableLossSupport arms loss t sample).card <= sparsity) → mu {sample | sparseLossPredictableVarianceAllHorizonRegretThreshold arms horizon sparsity delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta