BanditRLProof.Exp3BernsteinTuning

Learning rate balancing the entropy and pathwise estimator-square terms for the current high-probability budget.

noncomputable def bernsteinHighProbabilityLearningRate (K T gamma : Real) : Real

A cubic exploration budget makes one current Bernstein confidence radius at most `3 * gamma * T`.

theorem bernsteinConfidenceRadius_le_three_mul_gamma_mul_horizon (K T budget gamma : Real) (hK : 0 < K) (hT : 0 < T) (_hbudget : 0 <= budget) (hgamma_pos : 0 < gamma) (hgamma_le_one : gamma <= 1) (hcubic : K * budget <= gamma ^ 3 * T) : 2 * Real.sqrt (T * budget / (gamma / K)) + budget / (gamma / K) <= 3 * gamma * T

The bounded realized-loss deviation radius is at most `gamma * T` under its matching quadratic exploration budget.

theorem realizedDeviationRadius_le_mul_gamma_mul_horizon (T budget variance gamma : Real) (hT : 0 < T) (_hbudget : 0 <= budget) (_hvariance : 0 <= variance) (hgamma_pos : 0 < gamma) (hquadratic : 2 * variance * budget <= gamma ^ 2 * T) : Real.sqrt (2 * (T * variance) * budget) <= gamma * T

The tuned learning rate is positive in the nondegenerate finite-arm, positive-horizon regime.

theorem bernsteinHighProbabilityLearningRate_pos (K T gamma : Real) (hK_one : 1 < K) (hT : 0 < T) (hgamma_pos : 0 < gamma) : 0 < bernsteinHighProbabilityLearningRate K T gamma

Squared balance identity for the tuned learning rate.

theorem bernsteinHighProbabilityLearningRate_sq_mul (K T gamma : Real) (hK_one : 1 < K) (hT : 0 < T) (hgamma_pos : 0 < gamma) : bernsteinHighProbabilityLearningRate K T gamma ^ 2 * (T * K) = Real.log K * gamma

The cubic exploration contract places the tuned learning rate below the scale `gamma ^ 2 / K`.

theorem bernsteinHighProbabilityLearningRate_le_sq_div (K T gamma : Real) (hK_one : 1 < K) (hT : 0 < T) (hgamma_pos : 0 < gamma) (hcubic_log : K * Real.log K <= gamma ^ 3 * T) : bernsteinHighProbabilityLearningRate K T gamma <= gamma ^ 2 / K

The entropy contribution is at most `gamma * T` under the cubic arm-log budget.

theorem bernsteinEntropyBudget_le_mul_gamma_mul_horizon (K T gamma : Real) (hK_one : 1 < K) (hT : 0 < T) (hgamma_pos : 0 < gamma) (hcubic_log : K * Real.log K <= gamma ^ 3 * T) : Real.log K / bernsteinHighProbabilityLearningRate K T gamma <= gamma * T

Before the stability factor `1 / (1 - gamma)`, the pathwise square term has the same tuned scale as the entropy term.

theorem bernsteinUnscaledSquareBudget_le_mul_gamma_mul_horizon (K T gamma : Real) (hK_one : 1 < K) (hT : 0 < T) (hgamma_pos : 0 < gamma) (hcubic_log : K * Real.log K <= gamma ^ 3 * T) : bernsteinHighProbabilityLearningRate K T gamma * (T * (1 / (gamma / K))) <= gamma * T

The entropy and pathwise square terms together cost at most `3 * gamma * T` when `gamma <= 1 / 2`.

theorem bernsteinHedgeBudget_le_three_mul_gamma_mul_horizon (K T gamma : Real) (hK_one : 1 < K) (hT : 0 < T) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (hcubic_log : K * Real.log K <= gamma ^ 3 * T) : Real.log K / bernsteinHighProbabilityLearningRate K T gamma + (bernsteinHighProbabilityLearningRate K T gamma * (1 / (1 - gamma))) * (T * (1 / (gamma / K))) <= 3 * gamma * T

Dividing a total failure probability by three changes the logarithmic budget to `log (3 / delta)`.

theorem log_one_div_third_eq_log_three_div (delta : Real) (hdelta : 0 < delta) : Real.log (1 / (delta / 3)) = Real.log (3 / delta)

Under the explicit cubic and quadratic dominance contracts, the complete three-event realized Bernstein budget is at most `11 * gamma * T`.

theorem sampledPredictableBernsteinRealizedHighProbabilityRegretBudget_le_eleven_mul {Action : Type v} [DecidableEq Action] (arms : Finset Action) (hcard_two : 2 <= arms.card) (horizon : Nat) (hhorizon : 0 < horizon) (gamma delta : Real) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hcubic_log : (arms.card : Real) * Real.log (arms.card : Real) <= gamma ^ 3 * (horizon : Real)) (hcubic_confidence : (arms.card : Real) * Real.log (3 / delta) <= gamma ^ 3 * (horizon : Real)) (hquadratic_realized : 2 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (3 / delta) <= gamma ^ 2 * (horizon : Real)) : sampledPredictableBernsteinRealizedHighProbabilityRegretBudget arms (bernsteinHighProbabilityLearningRate (arms.card : Real) (horizon : Real) gamma) gamma horizon (delta / 3) <= 11 * gamma * (horizon : Real)

Tuned generated realized-regret tail with an explicit `11 * gamma * T` threshold. The current confidence route yields a `T^(2/3)`-type contract: the arm entropy and both importance-weighted confidence budgets must be dominated by `gamma ^ 3 * T`, while the bounded realized deviation uses the displayed quadratic contract.

theorem sampledPredictable_tunedBernsteinRealizedHighProbabilityRegret_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) (hdelta_le_one : delta <= 1) (hcubic_log : (arms.card : Real) * Real.log (arms.card : Real) <= gamma ^ 3 * (horizon : Real)) (hcubic_confidence : (arms.card : Real) * Real.log (3 / delta) <= gamma ^ 3 * (horizon : Real)) (hquadratic_realized : 2 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (3 / delta) <= gamma ^ 2 * (horizon : Real)) : let eta := bernsteinHighProbabilityLearningRate (arms.card : Real) (horizon : Real) gamma let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le (by linarith : gamma <= 1) loss.environment mu {sample | 11 * gamma * (horizon : Real) <= (Finset.range horizon).sum (fun t => sampledTrajectoryRealizedLossAt t sample) - (Finset.range horizon).sum (fun t => predictableLossAt loss t sample comparator)} <= ENNReal.ofReal delta