Lean module · EXP3
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovProbabilisticSparsityTuning
# Learning-rate tuning under probabilistic sparse losses This module tunes `eta` for the generated realized predictable-variance EXP3 route whose support-sparsity contract may fail with positive probability. The exact learning-rate scale is `S * T + sampledMixedSquaredPredictableVarianceRadius arms gamma v (delta / 5)`, where `v` is based on the unconditional `K * T` loss-mass envelope rather than the sparse `S * T` envelope. The final theorem preserves the exact generated sparsity-failure residual, and its practical consumer proves a `delta + epsilon` tail. Gamma remains caller-selected. This module does not transfer the pathwise sparse `14 * gamma * T` threshold to the probabilistic-sparsity setting.
Module map
Imports
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovProbabilisticSparsity
Imported by
BanditRLProof, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovProbabilisticSparsityExplicitTuning
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.probabilisticSparseLossPredictableVarianceBudget
Compiled
Markov threshold for cumulative predictable mixed-square variance when positive-probability sparsity failures require the global `K * T` envelope.
noncomputable def probabilisticSparseLossPredictableVarianceBudget {Action : Type v} [DecidableEq Action] (arms : Finset Action) (gamma : Real) (horizon : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.probabilisticSparseLossPredictableVarianceBudget_pos
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem probabilisticSparseLossPredictableVarianceBudget_pos {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 ≤ arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) : 0 < probabilisticSparseLossPredictableVarianceBudget arms gamma horizon delta
def
BanditRLProof.Exp3.probabilisticSparseLossPredictableVarianceHighProbabilityScale
Compiled
Complete Hedge scale with sparse observed-square mean and global Markov variance control.
noncomputable def probabilisticSparseLossPredictableVarianceHighProbabilityScale {Action : Type v} [DecidableEq Action] (arms : Finset Action) (gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.probabilisticSparseLossPredictableVarianceHighProbabilityScale_pos
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem probabilisticSparseLossPredictableVarianceHighProbabilityScale_pos {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 ≤ arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) : 0 < probabilisticSparseLossPredictableVarianceHighProbabilityScale arms gamma horizon sparsity delta
def
BanditRLProof.Exp3.probabilisticSparseLossPredictableVarianceHighProbabilityLearningRate
Compiled
Learning rate balancing entropy against the probabilistic-sparsity scale.
noncomputable def probabilisticSparseLossPredictableVarianceHighProbabilityLearningRate {Action : Type v} [DecidableEq Action] (arms : Finset Action) (gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.probabilisticSparseLossPredictableVarianceHighProbabilityLearningRate_pos
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem probabilisticSparseLossPredictableVarianceHighProbabilityLearningRate_pos {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 ≤ arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) : 0 < probabilisticSparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta
theorem
BanditRLProof.Exp3.probabilisticSparseLossPredictableVarianceHighProbabilityLearningRate_sq_mul_scale
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem probabilisticSparseLossPredictableVarianceHighProbabilityLearningRate_sq_mul_scale {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 ≤ arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) : probabilisticSparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta ^ 2 * probabilisticSparseLossPredictableVarianceHighProbabilityScale arms gamma horizon sparsity delta = Real.log (arms.card : Real)
theorem
BanditRLProof.Exp3.probabilisticSparseLossPredictableVarianceHighProbabilityHedgeBudget_le_three_mul_sqrt
Compiled
Under `gamma ≤ 1/2`, entropy and stability cost at most three copies of the balanced probabilistic-sparsity scale.
theorem probabilisticSparseLossPredictableVarianceHighProbabilityHedgeBudget_le_three_mul_sqrt {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 ≤ arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma ≤ 1 / 2) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) : Real.log (arms.card : Real) / probabilisticSparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta + (probabilisticSparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta * (1 / (1 - gamma))) * probabilisticSparseLossPredictableVarianceHighProbabilityScale arms gamma horizon sparsity delta ≤ 3 * Real.sqrt (Real.log (arms.card : Real) * probabilisticSparseLossPredictableVarianceHighProbabilityScale arms gamma horizon sparsity delta)
def
BanditRLProof.Exp3.probabilisticSparseLossPredictableVarianceRealizedMarkovTunedThreshold
Compiled
Tuned regret threshold retaining the global Markov variance radius and the three non-Hedge confidence terms.
noncomputable def probabilisticSparseLossPredictableVarianceRealizedMarkovTunedThreshold {Action : Type v} [DecidableEq Action] (arms : Finset Action) (gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictableVarianceSquareProbabilisticSparseLossRealizedMarkovHighProbabilityRegretBudget_le_tunedThreshold
Compiled
The raw probabilistic-sparsity budget is bounded by the eta-tuned threshold.
theorem sampledPredictableVarianceSquareProbabilisticSparseLossRealizedMarkovHighProbabilityRegretBudget_le_tunedThreshold {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 ≤ arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma ≤ 1 / 2) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) : sampledPredictableVarianceSquareProbabilisticSparseLossRealizedMarkovHighProbabilityRegretBudget arms (probabilisticSparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta) gamma horizon sparsity delta ≤ probabilisticSparseLossPredictableVarianceRealizedMarkovTunedThreshold arms gamma horizon sparsity delta
theorem
BanditRLProof.Exp3.sampledPredictable_tunedProbabilisticSparseLossPredictableVarianceRealizedMarkovRegret_tail
Compiled
Eta-tuned generated regret with the exact sparsity-failure residual.
theorem sampledPredictable_tunedProbabilisticSparseLossPredictableVarianceRealizedMarkovRegret_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) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma ≤ 1 / 2) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta : Real) (hdelta : 0 < delta) : let eta := probabilisticSparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le (by linarith : gamma ≤ 1) loss.environment mu {sample | probabilisticSparseLossPredictableVarianceRealizedMarkovTunedThreshold arms 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_tunedProbabilisticSparseLossPredictableVarianceRealizedMarkovRegret_tail_of_sparsityFailure_le
Compiled
Practical eta-tuned `delta + epsilon` theorem under an exact generated- measure bound on the sparsity-failure event.
theorem sampledPredictable_tunedProbabilisticSparseLossPredictableVarianceRealizedMarkovRegret_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) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma ≤ 1 / 2) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon sparsity : Nat) (hhorizon : 0 < horizon) (hsparsity : 0 < sparsity) (delta epsilon : Real) (hdelta : 0 < delta) : let eta := probabilisticSparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le (by linarith : gamma ≤ 1) loss.environment mu (sampledPredictableSparsityFailure arms loss horizon sparsity) ≤ ENNReal.ofReal epsilon → mu {sample | probabilisticSparseLossPredictableVarianceRealizedMarkovTunedThreshold arms 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