Lean module · EXP3
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsityAllHorizon
# All-horizon pathwise-variance EXP3 under probabilistic sparse losses The explicit pathwise-variance schedule has its refined `14 * gamma * T` threshold when four horizon inequalities make clipping inactive. Outside that regime this module uses the strict `T + 1` zero-probability threshold under exactly the same internal eta, gamma, and generated trajectory measure. The resulting theorem covers every positive horizon and preserves the exact support-sparsity failure residual. Its practical endpoint consumes `mu(sparsityFailure) <= ofReal epsilon` and returns `ofReal delta + ofReal epsilon`. The refined branch uses the sparse pathwise variance budget `K * S * T / gamma`. It does not reintroduce the global `K * T` Markov envelope, the old `K ^ 2` mixed numerator, or a polynomial `1 / delta` factor.
Module map
Imports
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsityExplicitTuning, BanditRLProof.Exp3BernsteinAllHorizon
Imported by
BanditRLProof, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsityBestArmAllHorizon
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.pathwiseVarianceProbabilisticSparseLossLargeHorizonCondition
Compiled
Regime in which all four components of the pathwise probabilistic-sparsity exploration schedule are at most one half.
def pathwiseVarianceProbabilisticSparseLossLargeHorizonCondition (K S T delta : Real) : Prop
def
BanditRLProof.Exp3.pathwiseVarianceProbabilisticSparseLossAllHorizonRegretThreshold
Compiled
All-horizon threshold for the pathwise probabilistic-sparsity route: use the explicit large-horizon threshold in its valid regime and `T + 1` otherwise.
noncomputable def pathwiseVarianceProbabilisticSparseLossAllHorizonRegretThreshold {Action : Type v} (arms : Finset Action) (horizon sparsity : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_allHorizonProbabilisticSparseLossPathwiseVarianceRealizedRegret_tail_off_sparsityFailure
Compiled
Generated all-horizon realized-regret theorem away from the exact support-sparsity failure event. Both branches use the same internally selected eta, gamma, and generated trajectory measure.
theorem sampledPredictable_allHorizonProbabilisticSparseLossPathwiseVarianceRealizedRegret_tail_off_sparsityFailure {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 := pathwiseVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) delta let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (pathwiseVarianceProbabilisticSparseLossClippedExplorationRate_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 (pathwiseVarianceProbabilisticSparseLossClippedExplorationRate_le_half (arms.card : Real) (sparsity : Real) (horizon : Real) delta).trans (by norm_num)) loss.environment mu ({sample | pathwiseVarianceProbabilisticSparseLossAllHorizonRegretThreshold arms horizon sparsity delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} \ sampledPredictableSparsityFailure arms loss horizon sparsity) <= ENNReal.ofReal delta
theorem
BanditRLProof.Exp3.sampledPredictable_allHorizonProbabilisticSparseLossPathwiseVarianceRealizedRegret_tail
Compiled
Generated all-horizon realized-regret theorem with the exact support-sparsity failure residual.
theorem sampledPredictable_allHorizonProbabilisticSparseLossPathwiseVarianceRealizedRegret_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 sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let gamma := pathwiseVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) delta let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (pathwiseVarianceProbabilisticSparseLossClippedExplorationRate_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 (pathwiseVarianceProbabilisticSparseLossClippedExplorationRate_le_half (arms.card : Real) (sparsity : Real) (horizon : Real) delta).trans (by norm_num)) loss.environment mu {sample | pathwiseVarianceProbabilisticSparseLossAllHorizonRegretThreshold 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 + mu (sampledPredictableSparsityFailure arms loss horizon sparsity)
theorem
BanditRLProof.Exp3.sampledPredictable_allHorizonProbabilisticSparseLossPathwiseVarianceRealizedRegret_tail_of_sparsityFailure_le
Compiled
Practical all-horizon `delta + epsilon` theorem under an exact bound on the support-sparsity failure event for the same internally tuned measure.
theorem sampledPredictable_allHorizonProbabilisticSparseLossPathwiseVarianceRealizedRegret_tail_of_sparsityFailure_le {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 epsilon : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let gamma := pathwiseVarianceProbabilisticSparseLossClippedExplorationRate (arms.card : Real) (sparsity : Real) (horizon : Real) delta let eta := pathwiseVarianceProbabilisticSparseLossHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (pathwiseVarianceProbabilisticSparseLossClippedExplorationRate_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 (pathwiseVarianceProbabilisticSparseLossClippedExplorationRate_le_half (arms.card : Real) (sparsity : Real) (horizon : Real) delta).trans (by norm_num)) loss.environment mu (sampledPredictableSparsityFailure arms loss horizon sparsity) <= ENNReal.ofReal epsilon → mu {sample | pathwiseVarianceProbabilisticSparseLossAllHorizonRegretThreshold 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 + ENNReal.ofReal epsilon