BanditRLProof.Exp3MixedSquareExponentialRealizedExplicitTuning

The mixed-square interval proxy is exactly `(K / (2 * gamma))^2`.

theorem sampledMixedSquaredVarianceProxy_coe_eq_card_div_two_gamma_sq {Action : Type v} (arms : Finset Action) (gamma : Real) (hgamma_pos : 0 < gamma) : ((sampledMixedSquaredVarianceProxy arms gamma : NNReal) : Real) = ((arms.card : Real) / (2 * gamma)) ^ 2

The logarithmically weighted mixed-square confidence radius is controlled by `gamma^2 T^2` under the sixth-power dominance contract.

theorem log_mul_sampledMixedSquaredConfidenceRadius_le_sq_mul_horizon_sq {Action : Type v} (arms : Finset Action) (gamma : Real) (hgamma_pos : 0 < gamma) (horizon : Nat) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hmixed : (arms.card : Real) ^ 2 * Real.log (arms.card : Real) ^ 2 * Real.log (4 / delta) / 2 <= gamma ^ 6 * (horizon : Real) ^ 3) : Real.log (arms.card : Real) * sampledMixedSquaredConfidenceRadius arms gamma horizon (delta / 4) <= gamma ^ 2 * (horizon : Real) ^ 2

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

theorem exponentialSquareBalancedSqrt_le_two_mul_gamma_mul_horizon {Action : Type v} (arms : Finset Action) (hcard_two : 2 <= arms.card) (gamma : Real) (hgamma_pos : 0 < gamma) (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) : Real.sqrt (Real.log (arms.card : Real) * exponentialSquareHighProbabilityScale arms gamma horizon delta) <= 2 * gamma * (horizon : Real)

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

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

Quadratic, sixth-power, cubic, and realized quadratic contracts reduce the learning-rate-tuned threshold to `14 * gamma * T`.

theorem exponentialSquareBernsteinRealizedTunedThreshold_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)) : exponentialSquareBernsteinRealizedTunedThreshold arms gamma horizon delta <= exponentialSquareBernsteinRealizedExplicitThreshold arms gamma horizon delta

Generated realized-regret tail under the four algebraic exploration contracts consumed by the explicit schedule below.

theorem sampledPredictable_gammaCharacterizedExponentialSquareBernsteinRealizedRegret_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 := exponentialSquareHighProbabilityLearningRate arms gamma horizon delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le (by linarith : gamma <= 1) loss.environment mu {sample | exponentialSquareBernsteinRealizedExplicitThreshold 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

Square-root component required by the armwise `K * T` part of the exponential-square scale.

noncomputable def exponentialSquareArmExplorationScale (K T : Real) : Real

Sixth-root component forced by the current interval variance proxy `(K / (2 * gamma))^2`.

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

Unclipped maximum of the arm, mixed-square, Bernstein-confidence, and realized-deviation exploration scales.

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

Explicit exploration schedule clipped into the Hedge stability regime.

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

A nonnegative sixth-root scale is at most one half when its numerator is at most one sixty-fourth of its positive denominator.

theorem rpow_inv_six_le_half_of_sixtyfour_mul_le (numerator denominator : Real) (hnumerator : 0 <= numerator) (hdenominator : 0 < denominator) (hlarge : 64 * numerator <= denominator) : (numerator / denominator) ^ (6 : Real)⁻¹ <= 1 / 2

If a sixth-root scale is below `gamma`, its numerator satisfies the corresponding sixth-power dominance contract.

theorem numerator_le_pow_six_mul_of_rpow_inv_six_le (numerator denominator gamma : Real) (hnumerator : 0 <= numerator) (hdenominator : 0 < denominator) (hroot : (numerator / denominator) ^ (6 : Real)⁻¹ <= gamma) : numerator <= gamma ^ 6 * denominator

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

theorem exponentialSquareBernsteinClippedExplorationRate_le_half (K T delta : Real) : exponentialSquareBernsteinClippedExplorationRate K T delta <= 1 / 2

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

theorem exponentialSquareBernsteinClippedExplorationRate_eq_raw (K T delta : Real) (hraw : exponentialSquareBernsteinRawExplorationRate K T delta <= 1 / 2) : exponentialSquareBernsteinClippedExplorationRate K T delta = exponentialSquareBernsteinRawExplorationRate K T delta

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

theorem exponentialSquareBernsteinRawExplorationRate_pos (K T delta : Real) (hK_one : 1 < K) (hT : 0 < T) : 0 < exponentialSquareBernsteinRawExplorationRate K T delta

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

theorem exponentialSquareBernsteinClippedExplorationRate_pos (K T delta : Real) (hK_one : 1 < K) (hT : 0 < T) : 0 < exponentialSquareBernsteinClippedExplorationRate K T delta

Four transparent horizon contracts ensure every raw schedule component is at most one half, hence clipping is inactive.

theorem exponentialSquareBernsteinRawExplorationRate_le_half_of_horizon_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) : exponentialSquareBernsteinRawExplorationRate K T delta <= 1 / 2

The clipped maximum satisfies exactly the four contracts consumed by the gamma-characterized tail theorem.

theorem exponentialSquareBernsteinClippedExplorationRate_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 := exponentialSquareBernsteinClippedExplorationRate 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 clipped maximum of the four exploration scales.

theorem sampledPredictable_explicitExponentialSquareBernsteinRealizedRegret_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 := exponentialSquareBernsteinClippedExplorationRate (arms.card : Real) (horizon : Real) delta let eta := exponentialSquareHighProbabilityLearningRate arms gamma horizon delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (exponentialSquareBernsteinClippedExplorationRate_pos (arms.card : Real) (horizon : Real) delta (by exact_mod_cast hcard_two) (by exact_mod_cast hhorizon)).le (by exact (exponentialSquareBernsteinClippedExplorationRate_le_half (arms.card : Real) (horizon : Real) delta).trans (by norm_num)) loss.environment mu {sample | exponentialSquareBernsteinRealizedExplicitThreshold 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