Lean module · EXP3
BanditRLProof.Exp3MixedSquareBernsteinRealizedTuning
# Learning-rate tuning for Bernstein-square realized EXP3 regret The variance-sensitive mixed-square route uses `K * T + sampledMixedSquaredBernsteinConfidenceRadius`. This module chooses the exact learning rate `eta = sqrt (log K / (K * T + squareRadius))` at the public four-event allocation. It balances entropy against the complete Bernstein-square stability scale. Exploration, the two action-confidence radii, and realized deviation remain explicit for a later gamma schedule.
Module map
Imports
BanditRLProof.Exp3MixedSquareBernsteinRealizedHighProbabilityRegret
Imported by
BanditRLProof, BanditRLProof.Exp3MixedSquareBernsteinRealizedExplicitTuning
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.bernsteinSquareHighProbabilityScale
Compiled
Positive scale appearing in the Bernstein-square Hedge term when the square event receives `delta / 4`.
noncomputable def bernsteinSquareHighProbabilityScale {Action : Type v} (arms : Finset Action) (gamma : Real) (horizon : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.bernsteinSquareHighProbabilityScale_pos
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem bernsteinSquareHighProbabilityScale_pos {Action : Type v} (arms : Finset Action) (hcard_two : 2 <= arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) : 0 < bernsteinSquareHighProbabilityScale arms gamma horizon delta
def
BanditRLProof.Exp3.bernsteinSquareHighProbabilityLearningRate
Compiled
Learning rate balancing entropy against the complete Bernstein-square stability scale at the public `delta / 4` square allocation.
noncomputable def bernsteinSquareHighProbabilityLearningRate {Action : Type v} (arms : Finset Action) (gamma : Real) (horizon : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.bernsteinSquareHighProbabilityLearningRate_pos
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem bernsteinSquareHighProbabilityLearningRate_pos {Action : Type v} (arms : Finset Action) (hcard_two : 2 <= arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) : 0 < bernsteinSquareHighProbabilityLearningRate arms gamma horizon delta
theorem
BanditRLProof.Exp3.bernsteinSquareHighProbabilityLearningRate_sq_mul_scale
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem bernsteinSquareHighProbabilityLearningRate_sq_mul_scale {Action : Type v} (arms : Finset Action) (hcard_two : 2 <= arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) : bernsteinSquareHighProbabilityLearningRate arms gamma horizon delta ^ 2 * bernsteinSquareHighProbabilityScale arms gamma horizon delta = Real.log (arms.card : Real)
theorem
BanditRLProof.Exp3.bernsteinSquareHighProbabilityHedgeBudget_le_three_mul_sqrt
Compiled
With `gamma <= 1/2`, entropy and the stability-amplified Bernstein-square scale cost at most three copies of their balanced square-root scale.
theorem bernsteinSquareHighProbabilityHedgeBudget_le_three_mul_sqrt {Action : Type v} (arms : Finset Action) (hcard_two : 2 <= arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) : Real.log (arms.card : Real) / bernsteinSquareHighProbabilityLearningRate arms gamma horizon delta + (bernsteinSquareHighProbabilityLearningRate arms gamma horizon delta * (1 / (1 - gamma))) * bernsteinSquareHighProbabilityScale arms gamma horizon delta <= 3 * Real.sqrt (Real.log (arms.card : Real) * bernsteinSquareHighProbabilityScale arms gamma horizon delta)
def
BanditRLProof.Exp3.bernsteinSquareRealizedTunedThreshold
Compiled
Explicit threshold after tuning all learning-rate-dependent terms. The exploration and three confidence contributions remain visible.
noncomputable def bernsteinSquareRealizedTunedThreshold {Action : Type v} (arms : Finset Action) (gamma : Real) (horizon : Nat) (delta : Real) : Real
theorem
BanditRLProof.Exp3.sampledPredictableBernsteinSquareRealizedHighProbabilityRegretBudget_le_tunedThreshold
Compiled
The complete Bernstein-square four-event realized budget is bounded by the learning-rate-tuned threshold.
theorem sampledPredictableBernsteinSquareRealizedHighProbabilityRegretBudget_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 : Nat) (hhorizon : 0 < horizon) (delta : Real) : sampledPredictableBernsteinSquareRealizedHighProbabilityRegretBudget arms (bernsteinSquareHighProbabilityLearningRate arms gamma horizon delta) gamma horizon (delta / 4) (delta / 4) (delta / 4) <= bernsteinSquareRealizedTunedThreshold arms gamma horizon delta
theorem
BanditRLProof.Exp3.sampledPredictable_tunedBernsteinSquareRealizedRegret_tail
Compiled
Generated realized-regret tail with the Bernstein-square-balanced learning rate. Gamma scheduling and confidence-radius simplification remain for downstream consumers.
theorem sampledPredictable_tunedBernsteinSquareRealizedRegret_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 : Nat) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) : let eta := bernsteinSquareHighProbabilityLearningRate arms gamma horizon delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le (by linarith : gamma <= 1) loss.environment mu {sample | bernsteinSquareRealizedTunedThreshold arms gamma horizon delta <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta