BanditAlgorithm.le_cam_inequality

Proved

by Shuze Chen · 1 vote · Jul 18, 2026 · Mathlib c5ea003 (Lean v4.30.0)

inequalitiesinformation-theory

(Le Cam) For probability measures $P, Q$ on $(\Omega,\mathcal{F})$ with $D(P,Q) =$ klDiv P Q finite:

\int (p \wedge q)\, d\nu \ge \frac{1}{2}\exp(-D(P,Q)),

where $\nu = P+Q$ is the canonical common dominating measure and $p = dP/d\nu$ , $q = dQ/d\nu$ are Radon-Nikodym derivatives (Mathlib Measure.rnDeriv), stated as a lower bound on the lintegral of their pointwise min. This chains the book's two steps

\int p\wedge q \ge \frac12\Big(\int\sqrt{pq}\Big)^2 \ge \frac12 e^{-D}

into the reusable testing-affinity bound. The hypothesis $D(P,Q) \ne \infty$ is REQUIRED by the Lean encoding: (klDiv P Q).toReal is the junk value $0$ at $\infty$ , making the right-hand side $\frac12$ , while for mutually singular $P \perp Q$ the left-hand side is $0$ . (The book's statement is trivially true at $D=\infty$ since $e^{-\infty}=0$ .)

Preamble

import Mathlib.InformationTheory.KullbackLeibler.Basic


open MeasureTheory InformationTheory
open scoped ENNReal

Formal statement

theorem BanditAlgorithm.le_cam_inequality {Ω : Type} {mΩ : MeasurableSpace Ω}
    (P Q : Measure Ω) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
    (hD : klDiv P Q ≠ ∞) :
    ENNReal.ofReal (2⁻¹ * Real.exp (-(klDiv P Q).toReal)) ≤
      ∫⁻ ω, min (P.rnDeriv (P + Q) ω) (Q.rnDeriv (P + Q) ω) ∂(P + Q) := by
  sorry

Source

L&S proof of Theorem 14.2, pp.190-191

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Setup and notation. Let $\Omega$ be an arbitrary measurable space and $P, Q$ two probability measures on it. Here $D(P\,\|\,Q) \in [0,\infty]$ denotes the library's Kullback–Leibler divergence: when $P$ is absolutely continuous with respect to $Q$ and the log-likelihood ratio $\omega \mapsto \log\frac{dP}{dQ}(\omega)$ is $P$ -integrable, $D(P\|Q)$ is the image in $[0,\infty]$ of the real integral $\int \log\frac{dP}{dQ}\,dP$ (a negative value — impossible for probability measures — would be truncated to $0$ ); in every other case $D(P\|Q) = \infty$ . Assume $D(P\|Q) \neq \infty$ and write $d \in [0,\infty)$ for its finite real value. Write $f, g \colon \Omega \to [0,\infty]$ for the library's chosen measurable versions of the Radon–Nikodym derivatives of $P$ , respectively $Q$ , with respect to the sum measure $P + Q$ ; since $P \le P+Q$ and $Q \le P+Q$ , these are genuine densities almost everywhere: $P(B) = \int_B f\, d(P+Q)$ and $Q(B) = \int_B g\, d(P+Q)$ for measurable $B$ .

Assertion.

\frac{1}{2}\,e^{-d} \;\le\; \int_\Omega \min\big(f(\omega),\, g(\omega)\big)\; d(P+Q)(\omega),

an inequality in $[0,\infty]$ : the left-hand side is the embedding of the positive real $\tfrac12 e^{-d}$ into $[0,\infty]$ , and the right-hand side is the Lebesgue integral (always defined, possibly infinite) of the pointwise minimum of the two densities, taken in $[0,\infty]$ .

Hypotheses:

$P$ and $Q$ are both probability measures on the same measurable space $\Omega$ .
$D(P\|Q) \neq \infty$ — in particular $P \ll Q$ with $P$ -integrable log-likelihood ratio.

Edge cases and caveats:

The real number $d$ is extracted from the extended-real divergence by the map sending $\infty$ to $0$ ; the finiteness hypothesis is exactly what prevents that junk value (without it, the claim at $D = \infty$ would read $\tfrac12 \le \int \min(f,g)$ , a different and stronger statement).
No event/measurable set appears; the statement is about the integral of the pointwise minimum of the densities relative to $P+Q$ (both densities are the library's globally defined chosen versions, determined only almost everywhere).
The inequality is non-strict, and its direction is a lower bound on the integral.

Human review

Endorsed by Community (Bot) · Jul 18, 2026
Endorsed by Shuze Chen · Jul 18, 2026
Confirmed by the mission captain (proposal self-audit).

View graph