Part IV — Lower Bounds for Bandits with Finitely Many Arms

Chapter 15: Minimax Lower Bounds

The frozen required body (§15.1–15.2) is compiled: Lemma 15.1 and Theorem 15.2 use one arbitrary randomized HistoryAlgorithm, the canonical finite-history law, exact unit-Gaussian construction and 1/27 constant, with worst-case and minimax consequences. Optional Exercise 15.7 remains partial: measurable-map KL contraction reuses Chapter 14's trim API, and the fixed-horizon observation corollary compiles; stopped-history information and F_tau factorization remain open. Notes and other exercises are outside the required-body completion contract.

Required body proofsCompiled

Required body coverageCompiled

Printed pp. 170–176PDF pp. 207–214

Source map

Bandit Algorithms, Tor Lattimore and Csaba Szepesvári, Cambridge University Press (2020), DOI 10.1017/9781108571401.

§15.1 Relative Entropy Between Bandits (CUP pp. 170–171 / author-online pp. 198–199 / PDF pp. 207–208; Lemma 15.1 and Eq. (15.1))
§15.2 Minimax Lower Bounds (CUP pp. 171–173 / author-online pp. 199–201 / PDF pp. 208–210; Theorem 15.2)
§15.3 Notes (CUP pp. 173–174 / author-online pp. 201–203 / PDF pp. 210–212)
§15.4 Bibliographic Remarks (CUP p. 174 / author-online p. 203 / PDF p. 212)
§15.5 Exercises (CUP pp. 174–176 / author-online pp. 203–205 / PDF pp. 212–214)

Section coverage

Section	Status	Formalization boundary
§15.1 Relative Entropy Between Bandits	Compiled	Lemma 15.1 and its same-policy adaptive-history KL decomposition compile.
§15.2 Minimax Lower Bounds	Compiled	The exact unit-Gaussian Theorem 15.2 existence and minimax chain compile with constant 1/27.
§15.3 Notes	Partial	Source mapping is present; the Bernoulli refinement is not formalized.
§15.4 Bibliographic Remarks	Source indexed	Mapped for reading context; it is not a Lean theorem target.
§15.5 Exercises	Partial	Exercise 15.7 has a compiled generic data-processing leaf and deterministic-history observation corollary; its stopped-history bound and final F_tau consumer, plus Exercises 15.1–15.6 and 15.8, are not formalized.

Open Chapter 15 at PDF p. 207

Learning goals

Keep Lemma 15.1's KL direction, first-law expectation, and same randomized policy fixed.
Compute the exact arm-level KL for equal-variance Gaussian alternatives.
Follow the compiled conditional-kernel chain rule and canonical randomized-policy history recursion that turn arm KL into first-law expected pull-count KL.
Follow the compiled least-explored-arm, testing-event, and Delta-tuning route through the exact 1/27 Theorem 15.2 terminal.
Separate Exercise 15.7's compiled measurable-observation data-processing leaf from its still-open stopped-history information bridge.

Necessary definitions and statements

Bandit-history divergence

Compiled

Bandit-history divergence. Formula renderer unavailable; readable fallback: The divergence compares finite action/reward histories generated by the same possibly randomized policy in two environments.\[D(\mathbb P_{\nu,\pi}^{(n)}\Vert\mathbb P_{\nu',\pi}^{(n)}).\]

Unit-variance Gaussian arm

Compiled

Unit-variance Gaussian arm. Formula renderer unavailable; readable fallback: Each arm is a real Gaussian probability law with the requested mean and variance exactly one.\[\nu_\mu=\mathcal N(\mu,1).\]

Equal-variance Gaussian KL

Compiled

Equal-variance Gaussian KL. Formula renderer unavailable; readable fallback: The relative entropy between unit-variance Gaussians is one half the squared difference of their means.\[D(\mathcal N(\mu,1)\Vert\mathcal N(\nu,1))=\frac{(\mu-\nu)^2}{2}.\]

Source minimax gap

Compiled

Source minimax gap. Formula renderer unavailable; readable fallback: The tuned gap makes the information exponent exactly one half and is at most one half when k-1 is at most n.\[\Delta=\sqrt{\frac{k-1}{4n}},\qquad\frac{2n\Delta^2}{k-1}=\frac12.\]

proof pseudocode

Minimax lower-bound proof flow

Choose the base instance
Set the first Gaussian mean to Delta and all other means to zero.
Find a least-explored alternative
Use the compiled Chapter 13 averaging leaf to choose i>1 with E[T_i(n)] at most n/(k-1).
Change one arm
Raise only arm i to mean 2 Delta; its compiled arm-level KL cost is 2 Delta squared.
Lift KL to histories
The compiled Lemma 15.1 route recursively applies the same-policy conditional-kernel chain rule and rewrites policy-arm masses as lower integrals of realized pull counts.
Test and tune
Apply Chapter 14 Bretagnolle–Huber to the source event T_1(n) at most n/2 (Lean's zero-based Fin 0 / T_0), choose Delta=sqrt((k-1)/(4n)), and use exp(-1/2) at least 16/27 to recover the exact 1/27 terminal.

Key source theorem and boundary

Source theorem · faithful restatement

Lemma 15.1 / Eq. (15.1) and Theorem 15.2

Original chapter ↗Compiled

The theorem converts indistinguishability of one-coordinate Gaussian alternatives into a finite-arm minimax regret obstruction.

Lemma 15.1 / Eq. (15.1) and Theorem 15.2. Formula renderer unavailable; readable fallback: History KL is the first-law expected sum of arm KL costs under one common policy; the Gaussian construction then yields regret at least one twenty-seventh times the square root of (k-1)n.\[D(\mathbb P_{\nu,\pi}^{(n)}\Vert\mathbb P_{\nu',\pi}^{(n)})=\sum_i\mathbb E_{\nu,\pi}[T_i(n)]D(P_i\Vert P_i'),\qquad R_n\ge\frac1{27}\sqrt{(k-1)n}.\]

Quantifier contract.

For every measurable, possibly randomized nonanticipating finite-history policy, there exists a unit-variance Gaussian environment.
Every environment mean lies in the unit cube [0,1]^k, with k>1 and n at least k-1.
The result bounds actual ENNReal expected pseudo-regret on the canonical generated history law; it is the standard Lemma 4.5-equivalent regret form used by the source.
Lean's inclusive lastRound contains lastRound+1 observations, so the n-round theorem is instantiated at lastRound=n-1.

Direct Lean endpoints.

Lean boundary. BanditRLProof.LowerBounds.banditHistoryRelativeEntropy_eq_expectedPulls_sum compiles Lemma 15.1 in the source KL direction with first-law realized expected pulls. BanditRLProof.LowerBounds.finiteArmedGaussianMinimaxLowerBound then compiles Theorem 15.2 for every randomized HistoryAlgorithm, k>1, and n at least k-1, returning a unit-cube mean vector and expected pseudo-regret at least sqrt((k-1)n)/27. The local inclusive lastRound contains lastRound+1 observations, so the n-round theorem uses lastRound=n-1.

Lean correspondence

Only declarations that exist in the current index and pass the verified build may render as compiled.

Lean declaration	Status	Role and exact type
`BanditRLProof.LowerBounds.klDiv_compProd_same_left_eq_lintegral_klDiv_of_measurable`	Compiled	General same-left composition-product KL chain rule, including singular fibres and infinite KL. Exact compact Lean statement theorem klDiv_compProd_same_left_eq_lintegral_klDiv_of_measurable {Base Target : Type*} [MeasurableSpace Base] [MeasurableSpace Target] [MeasurableSpace.CountablyGenerated Target] (mu : Measure Base) [IsFiniteMeasure mu] (kappa eta : Kernel Base Target) [IsMarkovKernel kappa] [IsMarkovKernel eta] (hmeasurable : Measurable (fun base => InformationTheory.klDiv (kappa base) (eta base))) : InformationTheory.klDiv (mu ⊗ₘ kappa) (mu ⊗ₘ eta) = ∫⁻ base, InformationTheory.klDiv (kappa base) (eta base) ∂mu
`BanditRLProof.LowerBounds.klDiv_historyStep_samePolicy_eq_iterated_lintegral_armKL_general`	Compiled	One randomized policy step contributes the first-law integral of the selected arm KL. Exact compact Lean statement theorem klDiv_historyStep_samePolicy_eq_iterated_lintegral_armKL_general {History Reward : Type*} {K : Nat} [MeasurableSpace History] [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (historyLaw : Measure History) [IsFiniteMeasure historyLaw] (policy : Kernel History (Fin K)) [IsMarkovKernel policy] (armLaw referenceArmLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] [IsMarkovKernel referenceArmLaw] : InformationTheory.klDiv (historyLaw ⊗ₘ (policy ⊗ₖ armLaw.comap Prod.snd measurable_snd)) (historyLaw ⊗ₘ (policy ⊗ₖ referenceArmLaw.comap Prod.snd measurable_snd)) = ∫⁻ history, ∫⁻ arm, InformationTheory.klDiv (armLaw arm) (referenceArmLaw arm) ∂policy history ∂historyLaw
`BanditRLProof.LowerBounds.canonicalBanditHistoryMeasure`	Compiled	Canonical finite action/reward history law for one randomized HistoryAlgorithm and stationary arm kernels. Exact compact Lean statement `noncomputable def canonicalBanditHistoryMeasure {K : Nat} {Reward : Type v} [MeasurableSpace Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] (n : Nat) : Measure (History.FinitePairHistory (Fin K) Reward n)`
`BanditRLProof.LowerBounds.canonicalRealizedExpectedPullCountThrough`	Compiled	First-law lower integral of the realized finite-history pull count. Exact compact Lean statement `noncomputable def canonicalRealizedExpectedPullCountThrough {K : Nat} {Reward : Type v} [MeasurableSpace Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] (n : Nat) (arm : Fin K) : ENNReal`
`BanditRLProof.LowerBounds.unitGaussianArm`	Compiled	Unit-variance Gaussian reward law. Exact compact Lean statement `abbrev unitGaussianArm (mu : Real) : Measure Real`
`BanditRLProof.LowerBounds.unitGaussianBandit`	Compiled	Finite family of unit-variance Gaussian arms indexed by a mean vector. Exact compact Lean statement `abbrev unitGaussianBandit {k : Nat} (mean : Fin k -> Real) : Fin k -> Measure Real`
`BanditRLProof.LowerBounds.log_gaussianPDFReal_div_gaussianPDFReal_one`	Compiled	Pointwise affine log-density ratio. Exact compact Lean statement `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`
`BanditRLProof.LowerBounds.llr_gaussianReal_one_ae`	Compiled	First-law almost-everywhere log Radon–Nikodym identity in the source direction. Exact compact Lean statement `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`
`BanditRLProof.LowerBounds.integrable_llr_gaussianReal_one`	Compiled	Integrability gate for the real KL integral. Exact compact Lean statement `theorem integrable_llr_gaussianReal_one (mu nu : Real) : Integrable (llr (unitGaussianArm mu) (unitGaussianArm nu)) (unitGaussianArm mu)`
`BanditRLProof.LowerBounds.klDiv_gaussianReal_one`	Compiled	Exact KL D(N(mu,1),N(nu,1))=(mu-nu)^2/2. Exact compact Lean statement `theorem klDiv_gaussianReal_one (mu nu : Real) : InformationTheory.klDiv (unitGaussianArm mu) (unitGaussianArm nu) = ENNReal.ofReal ((mu - nu) ^ 2 / 2)`
`BanditRLProof.LowerBounds.klDiv_unitGaussianArm_zero_two_mul`	Compiled	Source changed-arm cost D(N(0,1),N(2 Delta,1))=2 Delta squared. Exact compact Lean statement `theorem klDiv_unitGaussianArm_zero_two_mul (gap : Real) : InformationTheory.klDiv (unitGaussianArm 0) (unitGaussianArm (2 * gap)) = ENNReal.ofReal (2 * gap ^ 2)`
`BanditRLProof.LowerBounds.gaussianMinimaxGap`	Compiled	Source tuning Delta=sqrt(m/(4n)) over explicit real count and horizon parameters. Exact compact Lean statement `noncomputable def gaussianMinimaxGap (alternativeCount horizon : Real) : Real`
`BanditRLProof.LowerBounds.gaussianMinimaxGap_sq`	Compiled	Squared source gap identity under nonnegative parameters. Exact compact Lean statement `theorem gaussianMinimaxGap_sq {alternativeCount horizon : Real} (halternatives : 0 ≤ alternativeCount) (hhorizon : 0 ≤ horizon) : gaussianMinimaxGap alternativeCount horizon ^ 2 = alternativeCount / (4 * horizon)`
`BanditRLProof.LowerBounds.gaussianMinimaxGap_informationExponent_eq_half`	Compiled	Exact information exponent 2n Delta squared divided by m equals one half. Exact compact Lean statement `theorem gaussianMinimaxGap_informationExponent_eq_half {alternativeCount horizon : Real} (halternatives : 0 < alternativeCount) (hhorizon : 0 < horizon) : 2 * horizon * gaussianMinimaxGap alternativeCount horizon ^ 2 / alternativeCount = 1 / 2`
`BanditRLProof.LowerBounds.gaussianMinimaxGap_le_half`	Compiled	The horizon condition m at most n keeps Delta at most one half. Exact compact Lean statement `theorem gaussianMinimaxGap_le_half {alternativeCount horizon : Real} (hhorizon : 0 < horizon) (hcount_le : alternativeCount ≤ horizon) : gaussianMinimaxGap alternativeCount horizon ≤ 1 / 2`
`BanditRLProof.LowerBounds.banditHistoryRelativeEntropy_eq_expectedPulls_sum`	Compiled	Source-facing Lemma 15.1 identity: history KL equals the sum of first-law realized expected pulls times directed arm KL. Exact compact Lean statement theorem banditHistoryRelativeEntropy_eq_expectedPulls_sum {K : Nat} {Reward : Type v} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw referenceArmLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] [IsMarkovKernel referenceArmLaw] (lastRound : Nat) : InformationTheory.klDiv (canonicalBanditHistoryMeasure algorithm armLaw lastRound) (canonicalBanditHistoryMeasure algorithm referenceArmLaw lastRound) = ∑ arm : Fin K, canonicalRealizedExpectedPullCountThrough algorithm armLaw lastRound arm * InformationTheory.klDiv (armLaw arm) (referenceArmLaw arm)
`BanditRLProof.LowerBounds.klDiv_map_le`	Compiled	Generic finite-measure KL data processing under an arbitrary measurable observation, including infinite source KL. Exact compact Lean statement `theorem klDiv_map_le {Source Target : Type*} [MeasurableSpace Source] [MeasurableSpace Target] (mu nu : Measure Source) [IsFiniteMeasure mu] [IsFiniteMeasure nu] (observe : Source -> Target) (hobserve : Measurable observe) : InformationTheory.klDiv (mu.map observe) (nu.map observe) <= InformationTheory.klDiv mu nu`
`BanditRLProof.LowerBounds.klDiv_observedBanditHistory_le_expectedPulls_sum`	Compiled	Deterministic-horizon observation corollary combining data processing with Lemma 15.1; this is not the stopping-time Exercise 15.7 theorem. Exact compact Lean statement theorem klDiv_observedBanditHistory_le_expectedPulls_sum {K : Nat} {Reward : Type v} {Observation : Type w} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] [MeasurableSpace Observation] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw referenceArmLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] [IsMarkovKernel referenceArmLaw] (lastRound : Nat) (observe : History.FinitePairHistory (Fin K) Reward lastRound -> Observation) (hobserve : Measurable observe) : InformationTheory.klDiv ((canonicalBanditHistoryMeasure algorithm armLaw lastRound).map observe) ((canonicalBanditHistoryMeasure algorithm referenceArmLaw lastRound).map observe) <= ∑ arm : Fin K, canonicalRealizedExpectedPullCountThrough algorithm armLaw lastRound arm * InformationTheory.klDiv (armLaw arm) (referenceArmLaw arm)
`BanditRLProof.LowerBounds.UnitGaussianBanditEnvironment`	Compiled	Unit-cube mean vector with a certified optimal arm; its kernel is the unit-variance Gaussian family. Exact compact Lean statement `structure UnitGaussianBanditEnvironment (K : Nat) where`
`BanditRLProof.LowerBounds.gaussianExpectedPseudoRegret`	Compiled	Actual ENNReal expected pseudo-regret on the canonical generated history law. Exact compact Lean statement `noncomputable def gaussianExpectedPseudoRegret {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : UnitGaussianBanditEnvironment K) (lastRound : Nat) : ENNReal`
`BanditRLProof.LowerBounds.exists_gaussianMinimax_historyKL_le_half`	Compiled	Least-explored changed arm and Lemma 15.1 give history KL at most one half. Exact compact Lean statement theorem exists_gaussianMinimax_historyKL_le_half {m horizon : Nat} (hm : 0 < m) (hmhorizon : m ≤ horizon) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) : let gap := gaussianMinimaxGap (m : Real) (horizon : Real) ∃ i : Fin m, InformationTheory.klDiv (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel (gaussianMinimaxBaseMean gap)) (horizon - 1)) (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel (gaussianMinimaxChangedMean gap i)) (horizon - 1)) ≤ ENNReal.ofReal (1 / 2 : Real)
`BanditRLProof.LowerBounds.base_event_probability_lower_bound`	Compiled	The source event T_0(n) at most n/2 forces base-environment expected regret. Exact compact Lean statement theorem base_event_probability_lower_bound {m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (gap : Real) (hgap : 0 ≤ gap) (hgap_le : gap ≤ 1 / 2) (lastRound : Nat) : ENNReal.ofReal ((((lastRound + 1 : Nat) : Real) * gap / 2) * (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel (gaussianMinimaxBaseMean gap)) lastRound).real (gaussianMinimaxBaseSmallPullEvent (m := m) lastRound)) ≤ gaussianExpectedPseudoRegret algorithm (gaussianMinimaxBaseEnvironment gap hgap hgap_le) lastRound
`BanditRLProof.LowerBounds.changed_complement_probability_lower_bound`	Compiled	The complementary source event forces changed-environment expected regret. Exact compact Lean statement theorem changed_complement_probability_lower_bound {m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (gap : Real) (i : Fin m) (hgap : 0 ≤ gap) (hgap_le : gap ≤ 1 / 2) (lastRound : Nat) : ENNReal.ofReal ((((lastRound + 1 : Nat) : Real) * gap / 2) * (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel (gaussianMinimaxChangedMean gap i)) lastRound).real (gaussianMinimaxBaseSmallPullEvent (m := m) lastRound)ᶜ) ≤ gaussianExpectedPseudoRegret algorithm (gaussianMinimaxChangedEnvironment gap i hgap hgap_le) lastRound
`BanditRLProof.LowerBounds.sixteen_div_twentySeven_le_exp_neg_half`	Compiled	Rigorous exponential constant bound used to recover 1/27. Exact compact Lean statement `theorem sixteen_div_twentySeven_le_exp_neg_half : (16 / 27 : Real) ≤ Real.exp (-(1 / 2 : Real))`
`BanditRLProof.LowerBounds.finiteArmedGaussianMinimaxLowerBound`	Compiled	Source-facing Theorem 15.2 existence theorem for every randomized history policy. Exact compact Lean statement `theorem finiteArmedGaussianMinimaxLowerBound {k horizon : Nat} (hk : 1 < k) (hkhorizon : k - 1 ≤ horizon) (algorithm : Thompson.HistoryAlgorithm (Fin k) Real) : ∃ environment : UnitGaussianBanditEnvironment k, ENNReal.ofReal ((1 / 27 : Real) * Real.sqrt (((k - 1 : Nat) : Real) * (horizon : Real))) ≤ gaussianExpectedPseudoRegret algorithm environment (horizon - 1)`
`BanditRLProof.LowerBounds.unitGaussianMinimaxExpectedPseudoRegret_ge`	Compiled	Worst-case supremum and policy infimum form of the exact 1/27 theorem. Exact compact Lean statement `theorem unitGaussianMinimaxExpectedPseudoRegret_ge {k horizon : Nat} (hk : 1 < k) (hkhorizon : k - 1 ≤ horizon) : ENNReal.ofReal ((1 / 27 : Real) * Real.sqrt (((k - 1 : Nat) : Real) * (horizon : Real))) ≤ unitGaussianMinimaxExpectedPseudoRegret k (horizon - 1)`

Dependency graph

ch13Chapter 13 least-explored armCompiled

ch14Chapter 14 event testingCompiled

gaussianunit-Gaussian RN and arm KLCompiled

tuningsource gap and information exponentCompiled

conditionalconditional composition-product KL integralCompiled

policystochastic-policy canonical history lawCompiled

historyLemma 15.1 same-policy history KLCompiled

observation-dpiExercise 15.7 measurable-observation data-processing leafCompiled

stopped-historyExercise 15.7 stopped-history information bridgePlanned

minimaxTheorem 15.2 Gaussian 1/27 terminalCompiled

Reading path

Read Lemma 15.1 in §15.1 and verify D(nu,nu-prime), E_nu[T_i], and one common policy.
Inspect the conditional-kernel chain rule, canonical history recursion, and realized-count bridge before the source-facing Lemma 15.1 alias.
Read Theorem 15.2 in §15.2 and trace the base instance, least-explored alternative, source event T_1(n) at most n/2 (Lean Fin 0 / T_0), and Delta tuning.
Inspect the compiled event lower bounds, history-KL half bound, exponential constant, environment witness, and minimax corollary in that order.
For Exercise 15.7, inspect klDiv_map_le first, then keep the stopped-history KL and F_tau factorization as explicit remaining nodes.

Strict status and remaining gaps

The Bernoulli refinement discussed in the §15.3 Notes and Exercises 15.1–15.6 and 15.8 are outside the current compiled slice.
Exercise 15.7 is not complete: generic data processing compiles, but the stopped-history information bound and F_tau-measurable factorization remain planned.