BanditRLProof.Exp3RandomSquareBernsteinRealizedTuning

Learning rate balancing entropy against the Markov estimator-square term when the square event receives `delta / 4`.

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

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

theorem randomSquareHighProbabilityLearningRate_pos (K T delta : Real) (hK_one : 1 < K) (hT : 0 < T) (hdelta : 0 < delta) : 0 < randomSquareHighProbabilityLearningRate K T delta

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

theorem randomSquareHighProbabilityLearningRate_sq_mul (K T delta : Real) (hK_one : 1 < K) (hT : 0 < T) (hdelta : 0 < delta) : randomSquareHighProbabilityLearningRate K T delta ^ 2 * (T * K) = Real.log K * (delta / 4)

With `gamma <= 1/2`, the entropy and stability-amplified random-square terms cost at most three copies of their balanced square-root scale.

theorem randomSquareHighProbabilityHedgeBudget_le_three_mul_sqrt (K T gamma delta : Real) (hK_one : 1 < K) (hT : 0 < T) (hgamma_pos : 0 < gamma) (hgamma_le_half : gamma <= 1 / 2) (hdelta : 0 < delta) : Real.log K / randomSquareHighProbabilityLearningRate K T delta + (randomSquareHighProbabilityLearningRate K T delta * (1 / (1 - gamma))) * (K * T / (delta / 4)) <= 3 * Real.sqrt (4 * K * T * Real.log K / delta)

Explicit threshold after tuning only the learning-rate-dependent terms. The exploration and three confidence contributions remain visible.

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

The complete four-event realized budget is bounded by the explicit learning-rate-tuned threshold.

theorem sampledPredictableRandomSquareBernsteinRealizedHighProbabilityRegretBudget_le_tunedThreshold {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) : sampledPredictableRandomSquareBernsteinRealizedHighProbabilityRegretBudget arms (randomSquareHighProbabilityLearningRate (arms.card : Real) (horizon : Real) delta) gamma horizon (delta / 4) (delta / 4) (delta / 4) <= randomSquareBernsteinRealizedTunedThreshold arms gamma horizon delta

Generated realized-regret tail with the random-square learning rate. This optimizes the entropy/Markov-square pair while leaving the exploration-floor and realized-deviation confidence terms explicit.

theorem sampledPredictable_tunedRandomSquareBernsteinRealizedRegret_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) : 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 | randomSquareBernsteinRealizedTunedThreshold 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