Lean module · EXP3
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovAESparsityAllHorizon
# All-horizon sparse-loss EXP3 under almost-everywhere sparsity 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. The exceptional sparsity set has measure zero, so this transport spends no additional failure probability. The result still uses the armwise aggregate loss mass and Markov's polynomial confidence dependence; it is not a best-arm first-order or Freedman/EXP3.P theorem.
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.
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