Lean module · EXP3
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsity
# Pathwise sparse variance under probabilistic sparsity This module removes the global `arms.card * horizon` Markov envelope from the positive-probability sparsity route. Outside the explicit sparsity-failure event, the armwise loss mass is at most `sparsity * horizon`; the existing pointwise mixed-square variance inequality therefore gives the deterministic variance budget `(1 / (gamma / arms.card)) * (sparsity * horizon)`. The realized-regret proof uses four confidence events at `delta / 4`. The sparsity-failure event is charged exactly once, and no measurability assumption on that event is required.
Module map
Imports
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovProbabilisticSparsity
Imported by
BanditRLProof, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedDoublePathwiseVarianceProbabilisticSparsity, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsityTuning
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.sampledPredictableSparsePathwiseVarianceBudget
Compiled
Deterministic cumulative predictable-variance budget on trajectories that obey the requested support-cardinality cap.
noncomputable def sampledPredictableSparsePathwiseVarianceBudget {Action : Type v} [DecidableEq Action] (arms : Finset Action) (gamma : Real) (horizon sparsity : Nat) : Real
theorem
BanditRLProof.Exp3.sampledPredictableMixedSquaredVarianceSum_le_sparsePathwiseVarianceBudget_or_mem_sparsityFailure
Compiled
Every trajectory either obeys the sparse pathwise variance budget or lies in the explicit sparsity-failure event.
theorem sampledPredictableMixedSquaredVarianceSum_le_sparsePathwiseVarianceBudget_or_mem_sparsityFailure {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) (horizon sparsity : Nat) (sample : Env × ((k : Nat) → Action × Real)) : sampledPredictableMixedSquaredVarianceSum arms eta gamma loss horizon sample ≤ sampledPredictableSparsePathwiseVarianceBudget arms gamma horizon sparsity ∨ sample ∈ sampledPredictableSparsityFailure arms loss horizon sparsity
def
BanditRLProof.Exp3.sampledPredictableVarianceSquareProbabilisticSparseLossRealizedPathwiseVarianceHighProbabilityRegretBudget
Compiled
Four-event realized sparse-loss budget with deterministic pathwise predictable variance on the sparsity-good event.
noncomputable def sampledPredictableVarianceSquareProbabilisticSparseLossRealizedPathwiseVarianceHighProbabilityRegretBudget {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_predictableVarianceSquareProbabilisticSparseLossRealizedPathwiseVarianceHighProbabilityRegret_tail_off_sparsityFailure
Compiled
Generated realized regret away from the exact support-sparsity failure event. Only the four confidence events remain after removing the common sparsity-failure set.
theorem sampledPredictable_predictableVarianceSquareProbabilisticSparseLossRealizedPathwiseVarianceHighProbabilityRegret_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) (eta gamma : Real) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu ({sample | sampledPredictableVarianceSquareProbabilisticSparseLossRealizedPathwiseVarianceHighProbabilityRegretBudget arms eta gamma 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_predictableVarianceSquareProbabilisticSparseLossRealizedPathwiseVarianceHighProbabilityRegret_tail
Compiled
Generated realized regret under probabilistic sparsity and deterministic pathwise variance on the good event. The common support-sparsity failure set is added exactly once to the off-bad confidence tail.
theorem sampledPredictable_predictableVarianceSquareProbabilisticSparseLossRealizedPathwiseVarianceHighProbabilityRegret_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) (eta gamma : Real) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareProbabilisticSparseLossRealizedPathwiseVarianceHighProbabilityRegretBudget arms eta gamma 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_predictableVarianceSquareProbabilisticSparseLossRealizedPathwiseVarianceHighProbabilityRegret_tail_of_sparsityFailure_le
Compiled
Practical `delta + epsilon` consumer of the pathwise-variance residual theorem.
theorem sampledPredictable_predictableVarianceSquareProbabilisticSparseLossRealizedPathwiseVarianceHighProbabilityRegret_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) (eta gamma : Real) (heta : 0 < eta) (hgamma_pos : 0 < gamma) (hgamma_lt_one : gamma < 1) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta epsilon : Real) (hdelta : 0 < delta) (hfailure : (prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment) (sampledPredictableSparsityFailure arms loss horizon sparsity) ≤ ENNReal.ofReal epsilon) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareProbabilisticSparseLossRealizedPathwiseVarianceHighProbabilityRegretBudget arms eta gamma 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