Lean module · Foundations
BanditRLProof.LowerBounds.Minimax
# Finite-armed minimax lower-bound dependencies This file starts the source-faithful Chapter 15 spine for Lattimore--Szepesvári, Bandit Algorithms* (2020). The compiled surface currently proves the exact unit-variance Gaussian likelihood ratio and KL formula used in Theorem 15.2. It deliberately does **not** claim Lemma 15.1's adaptive-history divergence decomposition or Theorem 15.2. Those terminals require a common stochastic policy-kernel history law and a conditional composition-product KL integral; the repository currently has neither complete interface.
Module map
Imports
BanditRLProof.LowerBounds.InformationTheory
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
abbrev
BanditRLProof.LowerBounds.unitGaussianArm
Compiled
A unit-variance Gaussian arm with mean `mu`.
abbrev unitGaussianArm (mu : Real) : Measure Real
abbrev
BanditRLProof.LowerBounds.unitGaussianBandit
Compiled
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
theorem
BanditRLProof.LowerBounds.log_gaussianPDFReal_div_gaussianPDFReal_one
Compiled
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
theorem
BanditRLProof.LowerBounds.llr_gaussianReal_one_ae
Compiled
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
theorem
BanditRLProof.LowerBounds.integrable_llr_gaussianReal_one
Compiled
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)
theorem
BanditRLProof.LowerBounds.klDiv_gaussianReal_one
Compiled
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)
theorem
BanditRLProof.LowerBounds.klDiv_unitGaussianArm_zero_two_mul
Compiled
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)
def
BanditRLProof.LowerBounds.gaussianMinimaxGap
Compiled
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
theorem
BanditRLProof.LowerBounds.gaussianMinimaxGap_sq
Compiled
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)
theorem
BanditRLProof.LowerBounds.gaussianMinimaxGap_informationExponent_eq_half
Compiled
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
theorem
BanditRLProof.LowerBounds.gaussianMinimaxGap_le_half
Compiled
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