Lean module · EXP3
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovHighProbabilityRegret
# Sparse-loss control of realized predictable-variance EXP3 regret This module discharges the pathwise armwise loss-mass premise of the small-loss route from a per-round support-cardinality contract. The local proof route is: 1. restrict each predictable loss vector to its nonzero support in `arms`; 2. use the `[0,1]` loss range to bound its mass by the support cardinality; 3. sum a uniform support-cardinality bound over `Finset.range horizon`; 4. instantiate the compiled small-loss realized Markov theorem with `lossMassBudget = sparsity * horizon`. The primary generated theorem only requires the support contract almost everywhere under its exact trajectory measure. A compatibility theorem retains the stronger pathwise contract uniform over all generated samples. Neither surface asserts a best-arm first-order bound, tunes `eta` or `gamma`, or replaces Markov overflow.
Module map
Imports
BanditRLProof.Exp3MixedSquarePredictableVarianceSmallLossRealizedMarkovHighProbabilityRegret
Imported by
BanditRLProof, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovProbabilisticSparsity, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovTuning
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.sampledPredictableLossSupport
Compiled
Nonzero predictable-loss coordinates among the active arms at one time.
noncomputable def sampledPredictableLossSupport {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (arms : Finset Action) (loss : PredictableLossVector Env Action) (t : Nat) (sample : Env × ((k : Nat) → Action × Real)) : Finset Action
theorem
BanditRLProof.Exp3.sampledPredictableLossMassAt_le_supportCard
Compiled
The predictable loss mass at one time is at most the number of active nonzero loss coordinates.
theorem sampledPredictableLossMassAt_le_supportCard {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (arms : Finset Action) (loss : PredictableLossVector Env Action) (t : Nat) (sample : Env × ((k : Nat) → Action × Real)) : arms.sum (fun action => predictableLossAt loss t sample action) ≤ (sampledPredictableLossSupport arms loss t sample).card
theorem
BanditRLProof.Exp3.sampledPredictableLossMassSum_le_sparsity_mul_horizon_of_sample
Compiled
A per-round support-cardinality bound for one trajectory supplies its armwise loss-mass budget.
theorem sampledPredictableLossMassSum_le_sparsity_mul_horizon_of_sample {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)) (hsparse : ∀ t, t < horizon → (sampledPredictableLossSupport arms loss t sample).card ≤ sparsity) : sampledPredictableLossMassSum arms loss horizon sample ≤ (sparsity : Real) * (horizon : Real)
theorem
BanditRLProof.Exp3.sampledPredictableLossMassSum_le_sparsity_mul_horizon
Compiled
A uniform per-round support-cardinality bound supplies the pathwise armwise loss-mass budget used by the small-loss theorem.
theorem sampledPredictableLossMassSum_le_sparsity_mul_horizon {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (arms : Finset Action) (loss : PredictableLossVector Env Action) (horizon sparsity : Nat) (hsparse : ∀ sample t, t < horizon → (sampledPredictableLossSupport arms loss t sample).card ≤ sparsity) (sample : Env × ((k : Nat) → Action × Real)) : sampledPredictableLossMassSum arms loss horizon sample ≤ (sparsity : Real) * (horizon : Real)
def
BanditRLProof.Exp3.sampledPredictableVarianceSquareSparseLossRealizedMarkovHighProbabilityRegretBudget
Compiled
Sparse-loss specialization of the five-event realized regret budget.
noncomputable def sampledPredictableVarianceSquareSparseLossRealizedMarkovHighProbabilityRegretBudget {Action : Type v} [DecidableEq Action] (arms : Finset Action) (eta gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictable_predictableVarianceSquareSparseLossRealizedMarkovHighProbabilityRegret_tail_total_delta_of_ae_sparsity
Compiled
Realized predictable-variance EXP3 regret when the per-round nonzero-loss support-cardinality bound holds almost everywhere under the exact generated trajectory measure.
theorem sampledPredictable_predictableVarianceSquareSparseLossRealizedMarkovHighProbabilityRegret_tail_total_delta_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) (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) (hsparse : ∀ᵐ sample ∂(prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment), ∀ t, t < horizon → (sampledPredictableLossSupport arms loss t sample).card ≤ sparsity) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareSparseLossRealizedMarkovHighProbabilityRegretBudget 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
theorem
BanditRLProof.Exp3.sampledPredictable_predictableVarianceSquareSparseLossRealizedMarkovHighProbabilityRegret_tail_total_delta
Compiled
Backward-compatible pathwise sparse-loss wrapper. The stronger universal contract is converted to the generated-measure almost-everywhere contract used by the primary theorem.
theorem sampledPredictable_predictableVarianceSquareSparseLossRealizedMarkovHighProbabilityRegret_tail_total_delta {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) (hsparse : ∀ sample t, t < horizon → (sampledPredictableLossSupport arms loss t sample).card ≤ sparsity) : let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le hgamma_lt_one.le loss.environment mu {sample | sampledPredictableVarianceSquareSparseLossRealizedMarkovHighProbabilityRegretBudget 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