Part IV — Lower Bounds for Bandits with Finitely Many Arms

Chapter 14: Foundations of Information Theory

The source-faithful §14.2 relative-entropy and Bretagnolle–Huber spine is compiled. Entropy/source coding in §14.1 and full sub-sigma-algebra data processing remain outside this scoped gate.

PartialPrinted pp. 160–169PDF pp. 195–206

Source map

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

§14.1 Entropy and Optimal Coding (CUP starts p. 160 / author-online pp. 186–188 / PDF pp. 195–197; pedagogical mapping only)
§14.2 Relative Entropy (CUP starts p. 162 / author-online pp. 188–191 / PDF pp. 197–200; formal target window)
§14.3 Notes (CUP p. 165 / author-online pp. 191–194 / PDF pp. 200–203)
§14.4 Bibliographic Remarks (CUP p. 167 / author-online p. 194 / PDF p. 203)
§14.5 Exercises (CUP pp. 167–169 / author-online pp. 194–197 / PDF pp. 203–206)

Open the formal PDF

Learning goals

Read relative entropy as an extended-real, direction-sensitive comparison of probability measures.
Distinguish the absolutely-continuous log-likelihood branch from singular support mismatch.
Map a measurable event to Bernoulli probabilities without increasing KL.
Derive the unconditional Bretagnolle–Huber testing bound, including the exp(-infinity)=0 branch.
Keep general coding theory and adaptive bandit-history decomposition outside the compiled §14.2 window.

Necessary definitions and statements

Entropy and optimal coding

Planned

Entropy and optimal coding. Entropy is the expected information content of a discrete outcome and motivates the chapter's coding discussion.\[H(P)=-\sum_x P(x)\log P(x).\]

Extended-real relative entropy

Compiled

Extended-real relative entropy. Relative entropy is the expected log likelihood ratio when P is absolutely continuous with respect to Q, and infinity on support mismatch.\[D(P\Vert Q)=\int \log\!\left(\frac{dP}{dQ}\right)dP,\qquad D(P\Vert Q)=+\infty\text{ if }P\not\ll Q.\]

Bernoulli relative entropy

Compiled

Bernoulli relative entropy. The two-point specialization uses zero-mass terms equal to zero and infinity when P assigns positive mass where Q assigns none.\[d(p,q)=p\log\frac pq+(1-p)\log\frac{1-p}{1-q},\]

Bretagnolle–Huber testing scale

Compiled

Bretagnolle–Huber testing scale. The real-valued scale makes the source convention exponential of negative infinity equals zero explicit.\[s(D)=\begin{cases}\tfrac12 e^{-D},&D<\infty,\\0,&D=\infty.\end{cases}\]

proof pseudocode

Event-testing proof flow

Split the KL branches
Use Mathlib's exact absolute-continuity and log-likelihood integrability characterization; retain infinity on support mismatch.
Coarsen to one event
Restrict both measures to A and its complement and prove d(P(A),Q(A)) is at most D(P,Q).
Prove the binary bound
Lower-bound binary likelihood affinity by exp(-d/2), then compare squared affinity with the two testing errors.
Restore all endpoints
Handle Bernoulli zero/one support cases through the extended-real endpoint convention.
Lift to measures
Use antitonicity of the testing scale and Q(A complement)=1-Q(A) to obtain the source theorem in the P-to-Q KL direction.

Key source theorem and boundary

Source theorem · faithful restatement

Theorem 14.2 / Eq. (14.7) (Bretagnolle–Huber)

Compiled

Observing an event cannot make two laws easier to distinguish than their full relative entropy permits.

Theorem 14.2 / Eq. (14.7) (Bretagnolle–Huber). For two probability measures and any measurable event, the sum of the P error on A and the Q error on its complement is at least one half times exponential negative relative entropy.\[P(A)+Q(A^{\mathrm c})\ge\tfrac12\exp\{-D(P\Vert Q)\}\]

Lean boundary. BanditRLProof.LowerBounds.bretagnolleHuber compiles this unconditional measure/event theorem with D(P,Q), Q(A complement), and an explicit zero scale at infinite KL. It does not claim §14.1 source coding, full Exercise 14.10, or the Chapter 15 adaptive-history chain rule.

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.relativeEntropy`	Compiled	Extended-real alias of Mathlib measure KL in the source direction P to Q. Exact compact Lean statement `abbrev relativeEntropy {α : Type*} [MeasurableSpace α] (P Q : Measure α) : ENNReal`
`BanditRLProof.LowerBounds.relativeEntropy_of_absolutelyContinuous_of_integrable`	Compiled	Theorem 14.1 regular branch with Mathlib's finite-measure mass correction visible. Exact compact Lean statement `theorem relativeEntropy_of_absolutelyContinuous_of_integrable {α : Type*} [MeasurableSpace α] (P Q : Measure α) (hPQ : P ≪ Q) (hInt : Integrable (llr P Q) P) : relativeEntropy P Q = ENNReal.ofReal (∫ x, llr P Q x ∂P + Q.real univ - P.real univ)`
`BanditRLProof.LowerBounds.relativeEntropy_of_probability_absolutelyContinuous_of_integrable`	Compiled	Probability-measure log-likelihood integral specialization. Exact compact Lean statement `theorem relativeEntropy_of_probability_absolutelyContinuous_of_integrable {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (hPQ : P ≪ Q) (hInt : Integrable (llr P Q) P) : relativeEntropy P Q = ENNReal.ofReal (∫ x, llr P Q x ∂P)`
`BanditRLProof.LowerBounds.relativeEntropy_eq_top_of_not_absolutelyContinuous`	Compiled	Theorem 14.1 singular branch: support mismatch gives infinity. Exact compact Lean statement `theorem relativeEntropy_eq_top_of_not_absolutelyContinuous {α : Type*} [MeasurableSpace α] {P Q : Measure α} (hPQ : ¬ P ≪ Q) : relativeEntropy P Q = ∞`
`BanditRLProof.LowerBounds.relativeEntropy_ne_top_iff`	Compiled	Exact absolute-continuity and log-likelihood-integrability finiteness contract. Exact compact Lean statement `theorem relativeEntropy_ne_top_iff {α : Type*} [MeasurableSpace α] {P Q : Measure α} : relativeEntropy P Q ≠ ∞ ↔ P ≪ Q ∧ Integrable (llr P Q) P`
`BanditRLProof.LowerBounds.bernoulliRelativeEntropy`	Compiled	Equation (14.4) two-point KL with exact support endpoints. Exact compact Lean statement `abbrev bernoulliRelativeEntropy (p q : Real) : ENNReal`
`BanditRLProof.LowerBounds.rnDeriv_restrict_restrict`	Compiled	Radon–Nikodym derivative identity after restricting both laws to a measurable cell. Exact compact Lean statement `theorem rnDeriv_restrict_restrict {α : Type*} [MeasurableSpace α] {P Q : Measure α} [SigmaFinite P] [SigmaFinite Q] (hPQ : P ≪ Q) {A : Set α} (hA : MeasurableSet A) : (P.restrict A).rnDeriv (Q.restrict A) =ᵐ[Q.restrict A] P.rnDeriv Q`
`BanditRLProof.LowerBounds.relativeEntropy_restrict_add_compl`	Compiled	Exact KL decomposition across an event and its complement. Exact compact Lean statement `theorem relativeEntropy_restrict_add_compl {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsFiniteMeasure P] [IsFiniteMeasure Q] (hPQ : P ≪ Q) {A : Set α} (hA : MeasurableSet A) : relativeEntropy P Q = relativeEntropy (P.restrict A) (Q.restrict A) + relativeEntropy (P.restrict Aᶜ) (Q.restrict Aᶜ)`
`BanditRLProof.LowerBounds.bernoulliRelativeEntropy_event_le`	Compiled	Event-level binary data processing with P(A), Q(A) and D(P,Q). Exact compact Lean statement `theorem bernoulliRelativeEntropy_event_le {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsProbabilityMeasure P] [IsProbabilityMeasure Q] {A : Set α} (hA : MeasurableSet A) : bernoulliRelativeEntropy (P.real A) (Q.real A) ≤ relativeEntropy P Q`
`BanditRLProof.LowerBounds.binaryBretagnolleHuber`	Compiled	Two-atom Bretagnolle–Huber theorem including singular Bernoulli endpoints. Exact compact Lean statement `theorem binaryBretagnolleHuber {p q : Real} (hp : KLUCB.IsBernoulliParameter p) (hq : KLUCB.IsBernoulliParameter q) : bretagnolleHuberScale (bernoulliRelativeEntropy p q) ≤ p + (1 - q)`
`BanditRLProof.LowerBounds.bretagnolleHuberScale`	Compiled	Explicit real encoding of one-half exp(-D), with zero at D=infinity. Exact compact Lean statement `noncomputable def bretagnolleHuberScale (d : ENNReal) : Real`
`BanditRLProof.LowerBounds.bretagnolleHuberScale_antitone`	Compiled	The testing scale reverses the event data-processing inequality. Exact compact Lean statement `theorem bretagnolleHuberScale_antitone {d D : ENNReal} (h : d ≤ D) : bretagnolleHuberScale D ≤ bretagnolleHuberScale d`
`BanditRLProof.LowerBounds.bretagnolleHuber`	Compiled	Exact unconditional Theorem 14.2 measure/event terminal. Exact compact Lean statement `theorem bretagnolleHuber {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsProbabilityMeasure P] [IsProbabilityMeasure Q] {A : Set α} (hA : MeasurableSet A) : bretagnolleHuberScale (relativeEntropy P Q) ≤ P.real A + Q.real Aᶜ`

Dependency graph

klmeasure KL and RN branchesCompiled

eventevent-level binary data processingCompiled

binarybinary testing and endpoint analysisCompiled

bhmeasure Bretagnolle–Huber terminalCompiled

codingentropy and optimal codingPlanned

historysame-policy adaptive history KL (compiled in Chapter 15)Compiled

Reading path

Read Eq. (14.4), Eq. (14.5), Theorem 14.1, and Eq. (14.6) before the testing theorem.
Inspect relativeEntropy_ne_top_iff to see exactly where absolute continuity and integrability enter.
Follow the event restriction identity into bernoulliRelativeEntropy_event_le and verify the P-to-Q direction.
Read the binary endpoint theorem before the measure-level bretagnolleHuber terminal.
Continue to Chapter 15 for adaptive same-policy history divergence and finite-arm minimax construction.

Strict status and remaining gaps

Entropy, Huffman coding, and optimal source-coding results from §14.1 are not formalized by this lower-bound gate.
Full data processing for an arbitrary sub-sigma-algebra from Exercise 14.10 is not claimed; the compiled leaf is the event/binary specialization.
Adaptive-bandit history likelihood ratios and KL decomposition belong to Chapter 15; the scoped finite-arm same-policy identity now compiles there.