BanditAlgorithm.bretagnolle_huber_inequality

Proved

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

inequalitiesinformation-theorylower-bounds

(Bretagnolle–Huber, GOAL) Let $P$ and $Q$ be probability measures on the same measurable space $(\Omega, \mathcal{F})$ with $D(P,Q) =$ klDiv P Q finite, and let $A \in \mathcal{F}$ be measurable. Then

P(A) + Q(A^c) \ge \frac{1}{2}\exp(-D(P,Q)),

with probabilities as Measure.real. CRITICAL BOUNDARY: the hypothesis $D(P,Q) \ne \infty$ is REQUIRED — without it the Lean statement is FALSE, since (∞).toReal = 0 would make the right-hand side $\frac12$ while e.g. $P = \delta_0$ , $Q = \delta_1$ , $A = \{1\}$ gives $P(A)+Q(A^c) = 0$ . The book's statement is trivially true at $D = \infty$ (right-hand side $\frac12 e^{-\infty} = 0$ ); only the toReal junk-value encoding breaks.

Preamble

import Mathlib.InformationTheory.KullbackLeibler.Basic


open MeasureTheory InformationTheory Real
open scoped ENNReal

Formal statement

theorem BanditAlgorithm.bretagnolle_huber_inequality {Ω : Type} {mΩ : MeasurableSpace Ω}
    (P Q : Measure Ω) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
    {A : Set Ω} (hA : MeasurableSet A) (hD : klDiv P Q ≠ ∞) :
    2⁻¹ * exp (-(klDiv P Q).toReal) ≤ P.real A + Q.real Aᶜ := by
  sorry

Source

L&S Theorem 14.2, Eq. (14.7), p.190

Read-back

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

Setup and notation. Let $\Omega$ be an arbitrary measurable space, $P, Q$ two probability measures on it, and $A \subseteq \Omega$ a measurable set. 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 $P(A)$ and $Q(A^{\mathsf c})$ for the real-valued measures of $A$ and of its complement (the extended-nonnegative measure values converted to reals — finite here, since both are probability measures).

Assertion. As an inequality between real numbers,

\frac{1}{2}\, e^{-d} \;\le\; P(A) \;+\; Q\big(A^{\mathsf c}\big).

Hypotheses:

$P$ and $Q$ are both probability measures on the same measurable space $\Omega$ .
$A$ is a measurable subset of $\Omega$ (the claim is universally quantified over such $A$ ).
$D(P\|Q) \neq \infty$ — in particular $P \ll Q$ with $P$ -integrable log-likelihood ratio.

Edge cases and caveats:

$d$ is obtained from the extended-real divergence by the conversion that sends $\infty$ to $0$ ; the finiteness hypothesis blocks that junk case (without it, at $D = \infty$ the left side would evaluate to $\tfrac12$ , a stronger, unintendedly different claim).
The left-hand side $\tfrac12 e^{-d}$ is always strictly positive, so the statement is never vacuous under its hypotheses.
The inequality is non-strict; the right-hand side pairs $P$ on the set $A$ with $Q$ on the complement of $A$ .

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