LemmaStatement: 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.

The PAC-Bayes change-of-measure inequality

Statement

Let $(Θ, A)$ be a measurable space, let $π$ be a probability measure, and let $ρ$ be a probability measure absolutely continuous with respect to $π$ , meaning that $π (A) = 0$ implies $ρ (A) = 0$ for all $A \in A$ . Define $K L (ρ ∥ π) : = \sup_{P} \sum_{A \in P} ρ (A) \log \frac{ρ (A)}{π (A)},$ where $P$ ranges over finite measurable partitions of $Θ$ , a zero-numerator term is $0$ , and a positive numerator over a zero denominator is $+ \infty$ . For every bounded measurable $f : Θ \to R$ , $E_{θ \sim ρ} f (θ) \leq K L (ρ ∥ π) + \log E_{θ \sim π} \exp (f (θ)),$ with the inequality interpreted as vacuous when $K L (ρ ∥ π) = + \infty$ .

Statement references

PAC-Bayes priors, posteriors, and relative entropy: a posterior is absolutely continuous with respect to the prior, and $K L$ is the supremum over finite measurable partitions.

The natural logarithm as the inverse of the exponential function: $\log$ is the inverse of the real exponential on the positive reals.

Finite log-sum inequality with support and equality cases: for finite nonnegative vectors, the sum of coordinatewise relative-entropy terms is at least the corresponding aggregate term.

Alquier, User-friendly Introduction to PAC-Bayes Bounds, Chapter 2, Lemma 2.2: states the Donsker–Varadhan variational formula for bounded measurable functions.

Facts & Assumptions

Given: A measurable space $(Θ, A)$ , probability measures $π, ρ$ with $ρ ≪ π$ , and a bounded measurable $f : Θ \to R$ .

[F1]

$K L (ρ ∥ π)$ is the supremum over finite measurable partitions $P$ of $\sum_{A \in P} ρ (A) \log (ρ (A) / π (A))$ , with zero-numerator terms set to $0$ . PAC-Bayes priors, posteriors, and relative entropy

[F2]

If $a_{i}, b_{i} \geq 0$ , $A = \sum_{i} a_{i}$ , and $B = \sum_{i} b_{i}$ , then $\sum_{a_{i} > 0} a_{i} \log (a_{i} / b_{i}) \geq A \log (A / B)$ , with the stated support conventions. Finite log-sum inequality with support and equality cases

[F3]

The real exponential and natural logarithm are defined on the stated domains; the exponential is positive and increasing and satisfies $\exp (u + v) = \exp (u) \exp (v)$ , while the natural logarithm is increasing and satisfies $\log (x y) = \log x + \log y$ for positive $x, y$ . The real exponential function and the number $e$ by a power series, The natural logarithm as the inverse of the exponential function, The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , The exponential function is strictly increasing, The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm

[F4]

On a probability space, expectation is the Lebesgue integral; a real measurable function is integrable when its absolute value has finite integral. The nonnegative integral is monotone and positively homogeneous, and for a nonnegative simple function $s = \sum_{j} c_{j} 1_{A_{j}}$ its integral is $\sum_{j} c_{j} P (A_{j})$ . A constant $c \geq 0$ therefore has integral $c$ when $P (Θ) = 1$ . Probability measures and probability spaces, Expectation of a nonnegative or integrable random variable, Integrable real and complex functions, and their integrals, The nonnegative Lebesgue integral, Nonnegative simple measurable functions, The integral of a nonnegative simple function, Monotonicity and nonnegative homogeneity of the nonnegative integral

[F5]

For integrable real functions, expectation is linear and $∣ E g ∣ \leq E ∣ g ∣$ . Linearity, monotonicity, and the modulus bound for expectation

[F6]

Measurable functions are defined by measurable preimages; composition with a Borel measurable map preserves measurability, and a continuous real map has Borel preimages of Borel sets. A measurable function between measurable spaces, A continuous map has Borel preimages of Borel sets, Composition with a Borel measurable outer map preserves measurability

Proof

Given: The hypotheses in the Statement.

1.1F3F4F6given

If $g$ is bounded and measurable with $∣ g ∣ \leq C$ on either probability space, then $E ∣ g ∣ \leq \int C d P = C$ , so $g$ is integrable. If $g$ is finite-valued, writing its positive and negative parts on its finite level-set partition and applying the simple-integral formula in [F4] gives $E_{P} g = \sum_{j} g_{j} P (A_{j})$ . Since $f$ is measurable and $\exp$ is continuous by [F3], [F6] makes $\exp \circ f$ measurable; boundedness of $f$ gives $0 < \exp (- C) \leq E_{π} \exp (f) \leq \exp (C) < \infty$ for some $C \geq 0$ . We may assume $K L (ρ ∥ π) < \infty$ , since otherwise the claim is immediate.

2.1F2F3step 1.1given

First let $f$ be finite-valued, with values $f_{1}, \dots, f_{N}$ on the finite measurable partition $A_{1}, \dots, A_{N}$ . Put $p_{j} = π (A_{j})$ and $r_{j} = ρ (A_{j})$ . Absolute continuity gives $p_{j} = 0 \Rightarrow r_{j} = 0$ . For $a_{j} = r_{j}$ and $b_{j} = p_{j} \exp (f_{j})$ , the sums are $1$ and $E_{π} \exp (f)$ by step 1.1. Applying [F2] yields $\sum_{r_{j} > 0} r_{j} \log \frac{r_{j}}{p_{j} \exp (f_{j})} \geq - \log E_{π} \exp (f)$ .

2.2F3F4F5F6step 1.1construct

For each integer $n \geq 1$ , partition the bounded range of $f$ into finitely many half-open intervals of width at most $1 / n$ , including the final endpoint, and let $f_{n}$ equal each interval's left endpoint on its preimage. These preimages are measurable by [F6], and $∥ f_{n} - f ∥_{\infty} \leq 1 / n$ . By [F5] and step 1.1, $∣ E_{ρ} f_{n} - E_{ρ} f ∣ \leq 1 / n$ . Monotonicity and homogeneity in [F4], together with [F3], give $e^{- 1 / n} E_{π} e^{f} \leq E_{π} e^{f_{n}} \leq e^{1 / n} E_{π} e^{f}$ . The logarithms are defined by step 1.1 and [F3], and differ by at most $1 / n$ .

3.1F1F2step 1.1step 2.1algebra

Expanding the logarithm and using step 1.1, the left side of step 2.1 equals $\sum_{j} r_{j} \log (r_{j} / p_{j}) - E_{ρ} f$ . The first term is the divergence of this partition, hence at most $K L (ρ ∥ π)$ by [F1]. Rearrangement gives the claim for finite-valued $f$ .

4.1step 3.1step 2.2algebra∎

Apply step 3.1 to each $f_{n}$ and let $n \to \infty$ ; the two expectation terms converge by the bounds in step 2.2, proving the stated inequality for bounded measurable $f$ .

Depends on

Used by

The PAC-Bayes KL generalization bound Theorem

Dependency tree · two levels

59 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

Pierre Alquier, User-friendly Introduction to PAC-Bayes Bounds, Chapter 2, Lemma 2.2 (standard reference, not scraped)