Lean module · EXP3
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovTuning
# Learning-rate tuning for sparse-loss predictable-variance EXP3 regret This module chooses the learning rate for the compiled sparse-loss realized Markov route. With `L = sparsity * horizon`, the exact Hedge stability scale is `L + sampledMixedSquaredPredictableVarianceRadius arms gamma v (delta / 5)`, where `v = ((1 / (gamma / K)) * L) / (delta / 5)` is the Markov variance threshold used by the five-event theorem. The learning rate `eta = sqrt (log K / scale)` balances entropy against this full scale. Under `gamma <= 1 / 2`, the two learning-rate-dependent terms cost at most `3 * sqrt (log K * scale)`. The theorem remains a pathwise armwise sparse-loss result. It does not tune `gamma`, replace Markov overflow, or claim a best-arm first-order rate.
Module map
Imports
BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovHighProbabilityRegret
Imported by
BanditRLProof, BanditRLProof.Exp3MixedSquarePredictableVarianceSparseLossRealizedMarkovExplicitTuning
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.sparseLossPredictableVarianceBudget
Compiled
Markov threshold for cumulative predictable mixed-square variance under the sparse armwise loss-mass budget.
noncomputable def sparseLossPredictableVarianceBudget {Action : Type v} (arms : Finset Action) (gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sparseLossPredictableVarianceBudget_pos
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sparseLossPredictableVarianceBudget_pos {Action : Type v} (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) (hdelta : 0 < delta) : 0 < sparseLossPredictableVarianceBudget arms gamma horizon sparsity delta
def
BanditRLProof.Exp3.sparseLossPredictableVarianceHighProbabilityScale
Compiled
Complete sparse-loss Hedge scale at the public five-event allocation.
noncomputable def sparseLossPredictableVarianceHighProbabilityScale {Action : Type v} [DecidableEq Action] (arms : Finset Action) (gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sparseLossPredictableVarianceHighProbabilityScale_pos
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sparseLossPredictableVarianceHighProbabilityScale_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) (hdelta : 0 < delta) : 0 < sparseLossPredictableVarianceHighProbabilityScale arms gamma horizon sparsity delta
def
BanditRLProof.Exp3.sparseLossPredictableVarianceHighProbabilityLearningRate
Compiled
Learning rate balancing entropy against the complete sparse-loss predictable-variance scale.
noncomputable def sparseLossPredictableVarianceHighProbabilityLearningRate {Action : Type v} [DecidableEq Action] (arms : Finset Action) (gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sparseLossPredictableVarianceHighProbabilityLearningRate_pos
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sparseLossPredictableVarianceHighProbabilityLearningRate_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) (hdelta : 0 < delta) : 0 < sparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta
theorem
BanditRLProof.Exp3.sparseLossPredictableVarianceHighProbabilityLearningRate_sq_mul_scale
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sparseLossPredictableVarianceHighProbabilityLearningRate_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) (hdelta : 0 < delta) : sparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta ^ 2 * sparseLossPredictableVarianceHighProbabilityScale arms gamma horizon sparsity delta = Real.log (arms.card : Real)
theorem
BanditRLProof.Exp3.sparseLossPredictableVarianceHighProbabilityHedgeBudget_le_three_mul_sqrt
Compiled
With `gamma <= 1/2`, entropy and sparse-loss stability cost at most three copies of their balanced square-root scale.
theorem sparseLossPredictableVarianceHighProbabilityHedgeBudget_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) (hdelta : 0 < delta) : Real.log (arms.card : Real) / sparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta + (sparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta * (1 / (1 - gamma))) * sparseLossPredictableVarianceHighProbabilityScale arms gamma horizon sparsity delta ≤ 3 * Real.sqrt (Real.log (arms.card : Real) * sparseLossPredictableVarianceHighProbabilityScale arms gamma horizon sparsity delta)
def
BanditRLProof.Exp3.sparseLossPredictableVarianceRealizedMarkovTunedThreshold
Compiled
Explicit sparse-loss threshold after tuning every learning-rate-dependent term. Gamma and the three non-square confidence contributions remain visible.
noncomputable def sparseLossPredictableVarianceRealizedMarkovTunedThreshold {Action : Type v} [DecidableEq Action] (arms : Finset Action) (gamma : Real) (horizon sparsity : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictableVarianceSquareSparseLossRealizedMarkovHighProbabilityRegretBudget_le_tunedThreshold
Compiled
The complete sparse-loss Markov budget is bounded by the eta-tuned threshold.
theorem sampledPredictableVarianceSquareSparseLossRealizedMarkovHighProbabilityRegretBudget_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) (hdelta : 0 < delta) : sampledPredictableVarianceSquareSparseLossRealizedMarkovHighProbabilityRegretBudget arms (sparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta) gamma horizon sparsity delta ≤ sparseLossPredictableVarianceRealizedMarkovTunedThreshold arms gamma horizon sparsity delta
theorem
BanditRLProof.Exp3.sampledPredictable_tunedSparseLossPredictableVarianceRealizedMarkovRegret_tail
Compiled
Generated sparse-loss realized-regret tail with the exact predictable-variance-balanced learning rate.
theorem sampledPredictable_tunedSparseLossPredictableVarianceRealizedMarkovRegret_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) (hsparse : ∀ sample t, t < horizon → (sampledPredictableLossSupport arms loss t sample).card ≤ sparsity) : let eta := sparseLossPredictableVarianceHighProbabilityLearningRate arms gamma horizon sparsity delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le (by linarith : gamma ≤ 1) loss.environment mu {sample | sparseLossPredictableVarianceRealizedMarkovTunedThreshold 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