Part IV — Lower Bounds for Bandits with Finitely Many Arms

Chapter 15: Minimax Lower Bounds

Lemma 15.1 now compiles for finite arms, a countably generated reward space, arbitrary Markov arm laws, and one common randomized history policy. The unit-Gaussian dependency slice also compiles; Theorem 15.2 and the 1/27 minimax terminal remain blocked.

PartialPrinted 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)

Open the formal PDF

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 least-explored-arm, testing-event, and Delta-tuning route to Theorem 15.2 without upgrading blocked nodes.

Necessary definitions and statements

Bandit-history divergence

Compiled

Bandit-history divergence. 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. 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. 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. 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 T_1(n) at most n/2, then choose Delta=sqrt((k-1)/(4n)); this source-specific regret/event and constant assembly remains blocked.

Key source theorem and boundary

Source theorem · faithful restatement

Lemma 15.1 / Eq. (15.1) and Theorem 15.2

Partial

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. 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}.\]

Lean boundary. BanditRLProof.LowerBounds.banditHistoryRelativeEntropy_eq_expectedPulls_sum compiles the Lemma 15.1 identity in the source KL direction and with first-law realized expected pulls, under explicit finite-arm/countably-generated regularity and the repository's arbitrary randomized HistoryAlgorithm. The local inclusive lastRound contains lastRound+1 observations, so the source's positive n-round form uses lastRound=n-1. No local declaration is presented as Theorem 15.2 or its 1/27 terminal.

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.exists_gaussianBandit_expectedRegret_ge_one_div_twentySeven`	Blocked	Reserved exact Theorem 15.2 existence terminal; no declaration is claimed.No local declaration is indexed.

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

minimaxTheorem 15.2 Gaussian 1/27 terminalBlocked

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, event T_1(n) at most n/2, and Delta tuning.
Treat Lemma 15.1 as a compiled dependency, then keep the source-specific regret event and Theorem 15.2 constant assembly visibly open.

Strict status and remaining gaps

Theorem 15.2's base/alternative regret event identities and the bridge from the compiled ENNReal history KL to the source testing event.
The final exponential/constant calculation, caller-free 1/27 existence terminal, and its minimax corollary.
The Bernoulli refinement discussed in the §15.3 Notes and the stopping-time Exercise 15.7 are outside the current compiled slice.