BanditRLProof.Exp3MixedSquareBernsteinRealizedExplicitTuning

The deterministic mixed-square Bernstein variance coefficient is exactly `K^2 / gamma`.

theorem sampledMixedSquaredBernsteinVarianceCoefficient_eq_card_sq_div_gamma {Action : Type v} (arms : Finset Action) (hcard_two : 2 <= arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) : sampledMixedSquaredBernsteinVarianceCoefficient arms gamma = (arms.card : Real) ^ 2 / gamma

Under the existing arm, sixth-power mixed, and confidence contracts, the log-weighted Bernstein mixed-square radius is at most `3 * gamma^2 * T^2`. The first two copies control the square-root term; the third controls the linear `log_+ / epsilon` correction.

theorem log_mul_sampledMixedSquaredBernsteinConfidenceRadius_le_three_mul_sq_mul_horizon_sq {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) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hbase : (arms.card : Real) * Real.log (arms.card : Real) <= gamma ^ 2 * (horizon : Real)) (hmixed : (arms.card : Real) ^ 2 * Real.log (arms.card : Real) ^ 2 * Real.log (4 / delta) / 2 <= gamma ^ 6 * (horizon : Real) ^ 3) (hconfidence : (arms.card : Real) * Real.log (4 / delta) <= gamma ^ 3 * (horizon : Real)) : Real.log (arms.card : Real) * sampledMixedSquaredBernsteinConfidenceRadius arms gamma horizon (delta / 4) <= 3 * gamma ^ 2 * (horizon : Real) ^ 2

The armwise base term and the variance-sensitive mixed-square radius make the learning-rate-balanced square root at most `2 * gamma * T`.

theorem bernsteinSquareBalancedSqrt_le_two_mul_gamma_mul_horizon {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) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hbase : (arms.card : Real) * Real.log (arms.card : Real) <= gamma ^ 2 * (horizon : Real)) (hmixed : (arms.card : Real) ^ 2 * Real.log (arms.card : Real) ^ 2 * Real.log (4 / delta) / 2 <= gamma ^ 6 * (horizon : Real) ^ 3) (hconfidence : (arms.card : Real) * Real.log (4 / delta) <= gamma ^ 3 * (horizon : Real)) : Real.sqrt (Real.log (arms.card : Real) * bernsteinSquareHighProbabilityScale arms gamma horizon delta) <= 2 * gamma * (horizon : Real)

Explicit threshold after controlling the balanced square root and all three remaining confidence contributions by the exploration scale.

noncomputable def bernsteinSquareRealizedExplicitThreshold {Action : Type v} (_arms : Finset Action) (gamma : Real) (horizon : Nat) (_delta : Real) : Real

The existing quadratic, sixth-power, cubic, and realized quadratic contracts reduce the variance-sensitive tuned threshold to `14 * gamma * T`. The sixth-power contract is conservative for the new square-root term, while the arm and confidence contracts jointly control the linear correction.

theorem bernsteinSquareRealizedTunedThreshold_le_explicitThreshold {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) (hbase : (arms.card : Real) * Real.log (arms.card : Real) <= gamma ^ 2 * (horizon : Real)) (hmixed : (arms.card : Real) ^ 2 * Real.log (arms.card : Real) ^ 2 * Real.log (4 / delta) / 2 <= gamma ^ 6 * (horizon : Real) ^ 3) (hconfidence : (arms.card : Real) * Real.log (4 / delta) <= gamma ^ 3 * (horizon : Real)) (hrealized : 2 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (4 / delta) <= gamma ^ 2 * (horizon : Real)) : bernsteinSquareRealizedTunedThreshold arms gamma horizon delta <= bernsteinSquareRealizedExplicitThreshold arms gamma horizon delta

Generated realized-regret tail under the four algebraic exploration contracts.

theorem sampledPredictable_gammaCharacterizedBernsteinSquareRealizedRegret_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) (hbase : (arms.card : Real) * Real.log (arms.card : Real) <= gamma ^ 2 * (horizon : Real)) (hmixed : (arms.card : Real) ^ 2 * Real.log (arms.card : Real) ^ 2 * Real.log (4 / delta) / 2 <= gamma ^ 6 * (horizon : Real) ^ 3) (hconfidence : (arms.card : Real) * Real.log (4 / delta) <= gamma ^ 3 * (horizon : Real)) (hrealized : 2 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (4 / delta) <= gamma ^ 2 * (horizon : Real)) : 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 | bernsteinSquareRealizedExplicitThreshold 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

The variance-sensitive route reuses the already compiled four-scale clipped schedule.

noncomputable def bernsteinSquareClippedExplorationRate (K T delta : Real) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernsteinSquareClippedExplorationRate_pos (K T delta : Real) (hK_one : 1 < K) (hT : 0 < T) : 0 < bernsteinSquareClippedExplorationRate K T delta

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernsteinSquareClippedExplorationRate_le_half (K T delta : Real) : bernsteinSquareClippedExplorationRate K T delta <= 1 / 2

The reused clipped schedule satisfies all four contracts needed by the variance-sensitive gamma-characterized theorem.

theorem bernsteinSquareClippedExplorationRate_contracts (K T delta : Real) (hK_one : 1 < K) (hT : 0 < T) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hlarge_arm : 4 * (K * Real.log K) <= T) (hlarge_mixed : 64 * (K ^ 2 * Real.log K ^ 2 * Real.log (4 / delta) / 2) <= T ^ 3) (hlarge_confidence : 8 * (K * Real.log (4 / delta)) <= T) (hlarge_realized : 8 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (4 / delta) <= T) : let gamma := bernsteinSquareClippedExplorationRate K T delta 0 < gamma ∧ gamma <= 1 / 2 ∧ K * Real.log K <= gamma ^ 2 * T ∧ K ^ 2 * Real.log K ^ 2 * Real.log (4 / delta) / 2 <= gamma ^ 6 * T ^ 3 ∧ K * Real.log (4 / delta) <= gamma ^ 3 * T ∧ 2 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (4 / delta) <= gamma ^ 2 * T

Fully explicit generated realized-regret tail for the variance-sensitive route, using the reused clipped maximum of four exploration scales.

theorem sampledPredictable_explicitBernsteinSquareRealizedRegret_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) (loss : PredictableLossVector Env Action) (comparator : Action) (hcomparator : comparator ∈ arms) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hlarge_arm : 4 * ((arms.card : Real) * Real.log (arms.card : Real)) <= (horizon : Real)) (hlarge_mixed : 64 * ((arms.card : Real) ^ 2 * Real.log (arms.card : Real) ^ 2 * Real.log (4 / delta) / 2) <= (horizon : Real) ^ 3) (hlarge_confidence : 8 * ((arms.card : Real) * Real.log (4 / delta)) <= (horizon : Real)) (hlarge_realized : 8 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (4 / delta) <= (horizon : Real)) : let gamma := bernsteinSquareClippedExplorationRate (arms.card : Real) (horizon : Real) delta let eta := bernsteinSquareHighProbabilityLearningRate arms gamma horizon delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (bernsteinSquareClippedExplorationRate_pos (arms.card : Real) (horizon : Real) delta (by exact_mod_cast hcard_two) (by exact_mod_cast hhorizon)).le (by exact (bernsteinSquareClippedExplorationRate_le_half (arms.card : Real) (horizon : Real) delta).trans (by norm_num)) loss.environment mu {sample | bernsteinSquareRealizedExplicitThreshold 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