BanditRLProof.LowerBounds.Minimax

A unit-variance Gaussian arm with mean `mu`.

abbrev unitGaussianArm (mu : Real) : Measure Real

The finite family of unit-variance Gaussian arms indexed by a mean vector.

abbrev unitGaussianBandit {k : Nat} (mean : Fin k -> Real) : Fin k -> Measure Real

Pointwise log-density ratio for two unit-variance Gaussian laws.

theorem log_gaussianPDFReal_div_gaussianPDFReal_one (mu nu x : Real) : Real.log (gaussianPDFReal mu (1 : NNReal) x / gaussianPDFReal nu (1 : NNReal) x) = (mu - nu) * x + (nu ^ 2 - mu ^ 2) / 2

The log Radon--Nikodym derivative has the expected affine form under the first Gaussian law. The direction is `N(mu,1)` to `N(nu,1)`.

theorem llr_gaussianReal_one_ae (mu nu : Real) : llr (unitGaussianArm mu) (unitGaussianArm nu) =ᵐ[unitGaussianArm mu] fun x => (mu - nu) * x + (nu ^ 2 - mu ^ 2) / 2

The Gaussian log likelihood ratio is integrable under its first law.

theorem integrable_llr_gaussianReal_one (mu nu : Real) : Integrable (llr (unitGaussianArm mu) (unitGaussianArm nu)) (unitGaussianArm mu)

Exact KL divergence between unit-variance Gaussian laws: `D(N(mu,1),N(nu,1))=(mu-nu)^2/2`. The result is stated in `ENNReal`, matching Mathlib's measure-KL API and retaining the source direction even though this equal-variance value happens to be symmetric in the two means.

theorem klDiv_gaussianReal_one (mu nu : Real) : InformationTheory.klDiv (unitGaussianArm mu) (unitGaussianArm nu) = ENNReal.ofReal ((mu - nu) ^ 2 / 2)

Source-specialized Gaussian KL value for the changed arm in the proof of Theorem 15.2.

theorem klDiv_unitGaussianArm_zero_two_mul (gap : Real) : InformationTheory.klDiv (unitGaussianArm 0) (unitGaussianArm (2 * gap)) = ENNReal.ofReal (2 * gap ^ 2)

The source tuning `Delta=sqrt(m/(4n))`, written for positive real-valued alternative count `m` and horizon `n`. Natural-count consumers must discharge their cast and positivity obligations explicitly.

noncomputable def gaussianMinimaxGap (alternativeCount horizon : Real) : Real

Squared form of the Chapter 15 minimax gap choice.

theorem gaussianMinimaxGap_sq {alternativeCount horizon : Real} (halternatives : 0 ≤ alternativeCount) (hhorizon : 0 ≤ horizon) : gaussianMinimaxGap alternativeCount horizon ^ 2 = alternativeCount / (4 * horizon)

With the source tuning, the history-KL upper exponent `2*n*Delta^2/m` is exactly `1/2`. This is a numeric dependency only: it does not supply the history-KL upper bound itself.

theorem gaussianMinimaxGap_informationExponent_eq_half {alternativeCount horizon : Real} (halternatives : 0 < alternativeCount) (hhorizon : 0 < horizon) : 2 * horizon * gaussianMinimaxGap alternativeCount horizon ^ 2 / alternativeCount = 1 / 2

If the number of alternative arms is at most the horizon, the tuned gap is at most one half, so the source means `Delta` and `2*Delta` lie in the unit interval after nonnegativity is combined with this leaf.

theorem gaussianMinimaxGap_le_half {alternativeCount horizon : Real} (hhorizon : 0 < horizon) (hcount_le : alternativeCount ≤ horizon) : gaussianMinimaxGap alternativeCount horizon ≤ 1 / 2