TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Pinsker’s inequality with event-supremum total variation

Statement

Assume AC. For probability measures $P, Q$ on one measurable space, with $∥ P - Q ∥_{T V} : = \sup_{A} ∣ P (A) - Q (A) ∣,$ the event-supremum convention without a factor $1 / 2$ , $∥ P - Q ∥_{T V} \leq \sqrt{\frac{1}{2} D (P ∥ Q)} .$ If $P ≪̸ Q$ , the right side is $+ \infty$ by the definition of KL divergence.

Facts & Assumptions

Given: AC and probability measures $P, Q$ on the same measurable space.

[A1]

The Axiom of Choice: AC supplies the Radon–Nikodym construction used by the KL divergence.

[F1]

Kullback–Leibler divergence and Likelihood-ratio change of measure: if $P ≪̸ Q$ , then $D (P ∥ Q) = + \infty$ ; if $P ≪ Q$ with $r = d P / d Q$ , then $P (B) = \int_{B} r d Q$ for every measurable $B$ , so $\int r d Q = 1$ , and $D (P ∥ Q) = \int r \log r d Q$ with $0 \log 0 = 0$ and finite negative part.

[F2]

Total variation distance for probability laws: $∥ P - Q ∥_{T V} = \sup_{A} ∣ P (A) - Q (A) ∣ \in [0, 1]$ ; this convention has no factor $1 / 2$ .

[F3]

Jensen's integral inequality for a probability measure: for a probability measure, an integrable real function $f$ , and convex $φ$ with $φ \circ f$ integrable, $φ (\int f) \leq \int φ (f)$ .

[F4]

The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ , The integral logarithm satisfies $L^{'} (x) = 1 / x$ for $x > 0$ and $L (1) = 0$ , The integral logarithm $L$ is the published natural logarithm, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , and The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : the identity $L = \log$ transfers $L^{'} (x) = 1 / x$ to $\log^{'} (x) = 1 / x$ ; products and compositions obey the derivative rules; and the mean value theorem applies on closed subintervals of $(0, 1)$ . Also $t \log t \to 0$ as $t ↓ 0$ : for $s \geq 1$ , $0 \leq \log (s) / s \leq 2 / \sqrt{s}$ using $\log s = \int_{1}^{s} d u / u$ and $1 / u \leq 1 / \sqrt{u}$ .

Proof

1.1A1F1F3F4given

If $P ≪̸ Q$ or $D (P ∥ Q) = + \infty$ , the inequality is immediate. Otherwise let $r = d P / d Q$ and $φ (t) = t \log t$ for $t > 0$ , with $φ (0) = 0$ . By [F4] and the product rule, $φ^{''} (t) = 1 / t > 0$ for $t > 0$ . The mean value theorem in [F4] makes $φ^{'}$ increasing and hence $φ$ convex on $(0, \infty)$ . The limit in [F4] makes this extension continuous at zero, so $φ$ is convex on $[0, \infty)$ . Since $D (P ∥ Q)$ is finite and its negative part is bounded by [F1], $φ (r)$ is $Q$ -integrable. Jensen [F3] and $\int r d Q = 1$ give $D (P ∥ Q) = \int φ (r) d Q \geq φ (1) = 0$ .

2.1A1F1F3givenstep 1.1algebra

Fix a measurable event $A$ , and put $a = P (A)$ , $b = Q (A)$ . If $b \in {0, 1}$ , absolute continuity gives $a = b$ , so step 1.1 yields $D (P ∥ Q) \geq k (a, b) = 0$ . If $0 < b < 1$ , normalize $Q$ on $A$ and on $A^{c}$ . Their averages of $r$ are $a / b$ and $(1 - a) / (1 - b)$ . Applying [F3] on each normalized probability space and adding yields $D (P ∥ Q) \geq a \log \frac{a}{b} + (1 - a) \log \frac{1 - a}{1 - b} = : k (a, b),$ with $0 \log 0 = 0$ by continuity.

3.1F4step 2.1algebra

For fixed $0 < b < 1$ , define $g (a) = k (a, b) - 2 (a - b)^{2}$ on $[0, 1]$ . Differentiating by [F4] gives $g^{''} (a) = \frac{1}{a (1 - a)} - 4 = \frac{(2 a - 1)^{2}}{a (1 - a)} \geq 0$ on $(0, 1)$ . For $a, b \in (0, 1)$ with $a > b$ , the mean value theorem applied to $g^{'}$ on $[b, a]$ shows $g^{'} (a) \geq g^{'} (b) = 0$ , and applied to $g$ on $[b, a]$ shows $g (a) \geq g (b) = 0$ . For $a, b \in (0, 1)$ with $a < b$ , the same two applications on $[a, b]$ show $g^{'} (a) \leq g^{'} (b) = 0$ and $g (a) \geq g (b) = 0$ . The limit in [F4] makes $g$ continuous at $a = 0, 1$ , so the inequality extends to those endpoints. If $b = 0$ or $b = 1$ , absolute continuity gives $a = b$ and equality. Thus $k (a, b) \geq 2 (a - b)^{2}$ in every case.

4.1F2step 2.1step 3.1algebra∎

Combining steps 2.1 and 3.1 gives $D (P ∥ Q) \geq 2 ∣ P (A) - Q (A) ∣^{2}$ for every measurable $A$ . Since the square is increasing on $[0, 1]$ , its supremum is the square of the supremum; using [F2] yields $D (P ∥ Q) \geq 2 ∥ P - Q ∥_{T V}^{2}$ , which is the claimed inequality.

Depends on

Used by

Dependency tree · two levels

62 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Philippe Rigollet and Jan-Christian Hütter, High-Dimensional Statistics: Lecture Notes, Chapter 4, Lemma 4.8 (standard reference, not scraped)
John Duchi, Lecture Notes on Statistics and Information Theory, Chapter 8, §8.2.2; Chapter 2, Proposition 2.2.8 (standard reference, not scraped)