BanditRLProof.Exp3RandomSquareBernsteinRealizedExplicitTuning

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

theorem log_one_div_fourth_eq_log_four_div (delta : Real) (hdelta : 0 < delta) : Real.log (1 / (delta / 4)) = Real.log (4 / delta)

The threshold after controlling both exploration-floor Bernstein radii and the realized-deviation radius by the exploration scale.

noncomputable def randomSquareBernsteinRealizedExplicitThreshold {Action : Type v} (arms : Finset Action) (gamma : Real) (horizon : Nat) (delta : Real) : Real

Cubic and quadratic exploration contracts turn the three remaining confidence radii in the learning-rate-tuned threshold into `7 * gamma * T`; together with exploration bias this contributes `8 * gamma * T`.

theorem randomSquareBernsteinRealizedTunedThreshold_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) (hcubic_confidence : (arms.card : Real) * Real.log (4 / delta) <= gamma ^ 3 * (horizon : Real)) (hquadratic_realized : 2 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (4 / delta) <= gamma ^ 2 * (horizon : Real)) : randomSquareBernsteinRealizedTunedThreshold arms gamma horizon delta <= randomSquareBernsteinRealizedExplicitThreshold arms gamma horizon delta

Generated realized-regret tail after characterizing the remaining exploration parameter by one cubic and one quadratic dominance contract.

theorem sampledPredictable_gammaCharacterizedRandomSquareBernsteinRealizedRegret_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_confidence : (arms.card : Real) * Real.log (4 / delta) <= gamma ^ 3 * (horizon : Real)) (hquadratic_realized : 2 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (4 / delta) <= gamma ^ 2 * (horizon : Real)) : let eta := randomSquareHighProbabilityLearningRate (arms.card : Real) (horizon : Real) delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma hgamma_pos.le (by linarith : gamma <= 1) loss.environment mu {sample | randomSquareBernsteinRealizedExplicitThreshold 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

Cube-root scale required by both `delta / 4` importance-weighted Bernstein radii.

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

Square-root scale required by the `delta / 4` realized-deviation radius.

noncomputable def randomSquareBernsteinRealizedExplorationScale (T delta : Real) : Real

Unclipped exploration scale covering both remaining confidence contracts.

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

Explicit exploration schedule clipped into the Hedge stability regime.

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

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

theorem randomSquareBernsteinClippedExplorationRate_le_half (K T delta : Real) : randomSquareBernsteinClippedExplorationRate K T delta <= 1 / 2

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

theorem randomSquareBernsteinClippedExplorationRate_eq_raw (K T delta : Real) (hraw : randomSquareBernsteinRawExplorationRate K T delta <= 1 / 2) : randomSquareBernsteinClippedExplorationRate K T delta = randomSquareBernsteinRawExplorationRate K T delta

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

theorem randomSquareBernsteinRawExplorationRate_pos (K T delta : Real) (hK : 0 < K) (hT : 0 < T) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : 0 < randomSquareBernsteinRawExplorationRate K T delta

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

theorem randomSquareBernsteinClippedExplorationRate_pos (K T delta : Real) (hK : 0 < K) (hT : 0 < T) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : 0 < randomSquareBernsteinClippedExplorationRate K T delta

Transparent large-horizon conditions ensure clipping is inactive.

theorem randomSquareBernsteinRawExplorationRate_le_half_of_horizon_contracts (K T delta : Real) (hK : 0 < K) (hT : 0 < T) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hlarge_confidence : 8 * (K * Real.log (4 / delta)) <= T) (hlarge_realized : 8 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (4 / delta) <= T) : randomSquareBernsteinRawExplorationRate K T delta <= 1 / 2

The clipped schedule satisfies the exact cubic and quadratic contracts consumed by the characterized random-square theorem.

theorem randomSquareBernsteinClippedExplorationRate_contracts (K T delta : Real) (hK : 0 < K) (hT : 0 < T) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (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 := randomSquareBernsteinClippedExplorationRate K T delta 0 < gamma ∧ gamma <= 1 / 2 ∧ K * Real.log (4 / delta) <= gamma ^ 3 * T ∧ 2 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (4 / delta) <= gamma ^ 2 * T

Generated realized-regret tail for the explicit clipped maximum of the confidence cube-root and realized square-root scales.

theorem sampledPredictable_explicitRandomSquareBernsteinRealizedRegret_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_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 := randomSquareBernsteinClippedExplorationRate (arms.card : Real) (horizon : Real) delta let eta := randomSquareHighProbabilityLearningRate (arms.card : Real) (horizon : Real) delta let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (randomSquareBernsteinClippedExplorationRate_pos (arms.card : Real) (horizon : Real) delta (by positivity) (by exact_mod_cast hhorizon) hdelta hdelta_le_one).le (by exact (randomSquareBernsteinClippedExplorationRate_le_half (arms.card : Real) (horizon : Real) delta).trans (by norm_num)) loss.environment mu {sample | randomSquareBernsteinRealizedExplicitThreshold 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