Lean module · EXP3
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovProbabilisticSparsity
# Probabilistic sparse-loss control of realized predictable-variance EXP3 regret This module allows the per-round support-cardinality contract to fail on an explicit generated-trajectory event. On paths outside that event, sparsity still supplies the `sparsity * horizon` loss-mass budget used by the observed mixed-square and Hedge terms. The Markov variance closure instead uses the global `arms.card * horizon` loss-mass envelope, so the exceptional event costs its actual generated-measure probability without assuming it is null. The resulting theorem is a caller-parameterized `delta + epsilon` route. It does not retain the sharper sparse variance mean on exceptional paths and does not claim the tuned all-horizon `14 * gamma * horizon` threshold.
Module map
Imports
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovHighProbabilityRegret
Imported by
BanditRLProof, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovProbabilisticSparsityTuning, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedPathwiseVarianceProbabilisticSparsity
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.sampledPredictableSparsityFailure
Compiled
Generated trajectories on which the requested per-round support cap fails at some time before the horizon.
noncomputable def sampledPredictableSparsityFailure {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (arms : Finset Action) (loss : PredictableLossVector Env Action) (horizon sparsity : Nat) : Set (Env × ((k : Nat) → Action × Real))
theorem
BanditRLProof.Exp3.sampledPredictableLossMassSum_le_or_mem_sparsityFailure
Compiled
Every trajectory either obeys the sparse armwise loss-mass budget or lies in the explicit sparsity-failure event.
theorem sampledPredictableLossMassSum_le_or_mem_sparsityFailure {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (arms : Finset Action) (loss : PredictableLossVector Env Action) (horizon sparsity : Nat) (sample : Env × ((k : Nat) → Action × Real)) : sampledPredictableLossMassSum arms loss horizon sample ≤ (sparsity : Real) * (horizon : Real) ∨ sample ∈ sampledPredictableSparsityFailure arms loss horizon sparsity
theorem
BanditRLProof.Exp3.sampledPredictableLossMassSum_le_card_mul_horizon
Compiled
The number of nonzero active coordinates is always at most the number of active arms, giving a global pathwise loss-mass envelope.
theorem sampledPredictableLossMassSum_le_card_mul_horizon {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (arms : Finset Action) (loss : PredictableLossVector Env Action) (horizon : Nat) (sample : Env × ((k : Nat) → Action × Real)) : sampledPredictableLossMassSum arms loss horizon sample ≤ (arms.card : Real) * (horizon : Real)
def
BanditRLProof.Exp3.sampledPredictableGlobalVarianceMeanBudget
Compiled
Global predictable-variance mean envelope used when sparsity may fail with positive probability.
noncomputable def sampledPredictableGlobalVarianceMeanBudget {Action : Type v} [DecidableEq Action] (arms : Finset Action) (gamma : Real) (horizon : Nat) : Real
theorem
BanditRLProof.Exp3.sampledPredictableMixedSquaredVarianceLIntegral_le_globalLossMass
Compiled
The global `arms.card * horizon` loss-mass envelope closes the cumulative predictable-variance `lintegral` without any sparsity assumption.
theorem sampledPredictableMixedSquaredVarianceLIntegral_le_globalLossMass {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) → Action × Real))) [IsProbabilityMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma ≤ 1) (loss : PredictableLossVector Env Action) (horizon : Nat) : sampledPredictableMixedSquaredVarianceLIntegral mu arms eta gamma loss horizon ≤ ENNReal.ofReal (sampledPredictableGlobalVarianceMeanBudget arms gamma horizon)
def
BanditRLProof.Exp3.sampledPredictableVarianceSquareProbabilisticSparseLossRealizedMarkovHighProbabilityRegretBudget
Compiled
Realized sparse-loss budget with a global Markov variance envelope. The observed-square mean remains `sparsity * horizon`, while the variance overflow threshold uses `arms.card * horizon`.
noncomputable def sampledPredictableVarianceSquareProbabilisticSparseLossRealizedMarkovHighProbabilityRegretBudget {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_predictableVarianceSquareProbabilisticSparseLossRealizedMarkovHighProbabilityRegret_tail
Compiled
Generated realized regret with an explicit positive-probability sparsity failure event. The total tail is the ordinary five-event budget plus the exact generated measure of that event.
theorem sampledPredictable_predictableVarianceSquareProbabilisticSparseLossRealizedMarkovHighProbabilityRegret_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) (delta : Real) (hdelta : 0 < delta) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareProbabilisticSparseLossRealizedMarkovHighProbabilityRegretBudget 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_predictableVarianceSquareProbabilisticSparseLossRealizedMarkovHighProbabilityRegret_tail_of_sparsityFailure_le
Compiled
Practical `delta + epsilon` consumer of the explicit sparsity-failure residual theorem.
theorem sampledPredictable_predictableVarianceSquareProbabilisticSparseLossRealizedMarkovHighProbabilityRegret_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) (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 | sampledPredictableVarianceSquareProbabilisticSparseLossRealizedMarkovHighProbabilityRegretBudget 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