BanditRLProof.Exp3BernsteinExplicitTuning

Cube-root scale required by the arm-entropy term.

noncomputable def bernsteinArmEntropyExplorationScale (K T : Real) : Real

Cube-root scale required by both importance-weighted Bernstein radii.

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

Square-root scale required by the bounded realized-deviation radius.

noncomputable def bernsteinRealizedExplorationScale (T delta : Real) : Real

Unclipped exploration scale simultaneously covering arm entropy, the two importance-weighted confidence radii, and the realized-deviation radius.

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

Explicit exploration schedule, clipped into the stability regime `gamma <= 1 / 2`.

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

A cube-root scale is at most one half when its numerator is at most one eighth of the positive horizon.

theorem rpow_inv_three_le_half_of_eight_mul_le (numerator T : Real) (hnumerator : 0 <= numerator) (hT : 0 < T) (hlarge : 8 * numerator <= T) : (numerator / T) ^ (3 : Real)⁻¹ <= 1 / 2

A square-root scale is at most one half when its numerator is at most one quarter of the positive horizon.

theorem sqrt_div_le_half_of_four_mul_le (numerator T : Real) (hT : 0 < T) (hlarge : 4 * numerator <= T) : Real.sqrt (numerator / T) <= 1 / 2

If the cube-root scale is below `gamma`, then the corresponding numerator obeys the cubic dominance contract.

theorem numerator_le_cube_mul_of_rpow_inv_three_le (numerator T gamma : Real) (hnumerator : 0 <= numerator) (hT : 0 < T) (hroot : (numerator / T) ^ (3 : Real)⁻¹ <= gamma) : numerator <= gamma ^ 3 * T

If the square-root scale is below `gamma`, then the corresponding numerator obeys the quadratic dominance contract.

theorem numerator_le_sq_mul_of_sqrt_div_le (numerator T gamma : Real) (hnumerator : 0 <= numerator) (hT : 0 < T) (hroot : Real.sqrt (numerator / T) <= gamma) : numerator <= gamma ^ 2 * T

The clipped schedule never exceeds the stability threshold.

theorem bernsteinClippedExplorationRate_le_half (K T delta : Real) : bernsteinClippedExplorationRate K T delta <= 1 / 2

If the raw schedule is already stable, clipping leaves it unchanged.

theorem bernsteinClippedExplorationRate_eq_raw (K T delta : Real) (hraw : bernsteinRawExplorationRate K T delta <= 1 / 2) : bernsteinClippedExplorationRate K T delta = bernsteinRawExplorationRate K T delta

The raw schedule is positive as soon as there are at least two arms and the horizon is positive.

theorem bernsteinRawExplorationRate_pos (K T delta : Real) (hK_one : 1 < K) (hT : 0 < T) : 0 < bernsteinRawExplorationRate K T delta

The clipped schedule remains positive in the nondegenerate finite-arm, positive-horizon regime.

theorem bernsteinClippedExplorationRate_pos (K T delta : Real) (hK_one : 1 < K) (hT : 0 < T) : 0 < bernsteinClippedExplorationRate K T delta

Three transparent horizon inequalities ensure that every raw component is at most one half, so the clipping branch is inactive.

theorem bernsteinRawExplorationRate_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 : 8 * (K * Real.log K) <= T) (hlarge_confidence : 8 * (K * Real.log (3 / delta)) <= T) (hlarge_realized : 8 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (3 / delta) <= T) : bernsteinRawExplorationRate K T delta <= 1 / 2

Under the large-horizon regime, the clipped schedule satisfies positivity, stability, both cubic dominance contracts, and the realized quadratic dominance contract required by the tuned tail theorem.

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

Generated realized-regret tail for the explicit clipped maximum of the two cube-root Bernstein scales and the realized square-root scale. The three large-horizon premises are sufficient conditions ensuring that clipping is inactive and all contracts of the characterized `11 * gamma * T` theorem hold.

theorem sampledPredictable_explicitBernsteinRealizedHighProbabilityRegret_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 : 8 * ((arms.card : Real) * Real.log (arms.card : Real)) <= (horizon : Real)) (hlarge_confidence : 8 * ((arms.card : Real) * Real.log (3 / delta)) <= (horizon : Real)) (hlarge_realized : 8 * ((Concentration.intervalVarianceProxy 0 1 : NNReal) : Real) * Real.log (3 / delta) <= (horizon : Real)) : let gamma := bernsteinClippedExplorationRate (arms.card : Real) (horizon : Real) delta let eta := bernsteinHighProbabilityLearningRate (arms.card : Real) (horizon : Real) gamma let mu := prior ⊗ₘ sampledImportanceWeightedTrajectoryKernel arms harms eta gamma (bernsteinClippedExplorationRate_pos (arms.card : Real) (horizon : Real) delta (by exact_mod_cast hcard_two) (by exact_mod_cast hhorizon)).le (by exact (bernsteinClippedExplorationRate_le_half (arms.card : Real) (horizon : Real) delta).trans (by norm_num)) 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