TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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 KL generalization bound

Statement

Let $(Θ, A)$ and $(Z, B)$ be measurable spaces. Let $π$ and $D$ be probability measures on them, respectively. Let $C \geq 0$ and let $ℓ : Θ \times Z \to [0, C]$ be measurable with respect to $A \otimes B$ . Let $m \geq 1$ and let $S = (Z_{1}, \dots, Z_{m})$ consist of independent observations with common law $D$ , equivalently having product law $D^{m}$ . Define $R (θ) : = \int_{Z} ℓ (θ, z) D (d z), {\hat{R}}_{S} (θ) : = \frac{1}{m} \sum_{i = 1}^{m} ℓ (θ, Z_{i}) .$ Fix the prior $π$ independently of $S$ , and fix $λ > 0$ and $δ \in (0, 1)$ . For a probability measure $ρ$ with $ρ ≪ π$ (that is, $π (A) = 0$ implies $ρ (A) = 0$ for all measurable $A$ ), define $K L (ρ ∥ π) : = \sup_{P} \sum_{A \in P} ρ (A) \log \frac{ρ (A)}{π (A)},$ where $P$ ranges over finite measurable partitions of $Θ$ , terms with zero numerator are $0$ , and a positive numerator over zero denominator is $+ \infty$ . With probability at least $1 - δ$ over $S$ , simultaneously for every such posterior $ρ$ , $E_{θ \sim ρ} R (θ) \leq E_{θ \sim ρ} {\hat{R}}_{S} (θ) + \frac{λ C^{2}}{8 m} + \frac{K L (ρ ∥ π) + \log (1 / δ)}{λ} .$ An infinite relative entropy makes the bound vacuous. The conclusion bounds posterior-average risk, not the risk of every posterior draw.

Statement references

PAC-Bayes priors, posteriors, and relative entropy: defines a sample-independent prior, an absolutely continuous posterior, and relative entropy.

Population and empirical risk: population risk is the expected loss and empirical risk is the sample-average loss.

Identical distribution and IID families: IID observations are independent and have a common law.

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

The real exponential function and the number $e$ by a power series: the real exponential is defined on all real inputs and $e = \exp (1)$ .

The Hoeffding MGF bound for a variable in a unit interval: a unit-range random variable has centered exponential moment at most $\exp (t^{2} / 8)$ for every real $t$ .

Alquier, User-friendly Introduction to PAC-Bayes Bounds, Chapter 2, Theorem 2.1 and proof: proves the bounded-loss PAC-Bayes KL bound by integrating the fixed-parameter Hoeffding MGF, applying the Donsker–Varadhan formula, and using Markov's inequality.

Facts & Assumptions

Given: The probability spaces, loss, product-law sample, $m, C, λ, δ$ , and fixed prior in the Statement.

[A1]

The prior $π$ is fixed independently of the sample; the loss satisfies $0 \leq ℓ (θ, z) \leq C$ and is product-measurable; $m \geq 1$ , $λ > 0$ , and $0 < δ < 1$ .

[F1]

In a supervised prediction problem, population risk is the expectation of the supervised loss and empirical risk is its sample average; for a fixed measurable predictor these are defined, and the empirical-risk function of the sample is measurable. Population and empirical risk, Population and empirical risks are measurable

[F2]

IID means independent random elements with a common law. Identical distribution and IID families

[F3]

Measurable functions of independent random elements remain independent. Measurable coordinatewise functions preserve independence

[F4]

If $Z_{i}$ has law $D$ , then $E ℓ (θ, Z_{i}) = \int ℓ (θ, z) D (d z) = R (θ)$ . Change of variables for expectation

[F5]

For an integrable real random variable, expectation is homogeneous: $E (a X) = a E X$ . Linearity, monotonicity, and the modulus bound for expectation

[F6]

If $0 \leq Y \leq 1$ , then $E \exp (t (Y - E Y)) \leq \exp (t^{2} / 8)$ for every real $t$ . The proof of this supplier is choice-free. The Hoeffding MGF bound for a variable in a unit interval

[F7]

Expectations of finite products of nonnegative functions of independent real random variables factor as products of expectations, and the exponential of a finite sum is the product of the exponentials. Expectations factor over finite products of independent random variables, The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$

[F8]

$π$ and $D$ are probability measures; finite product sigma-algebras and finite products of probability measures are defined, the product measure has the rectangle formula, and Tonelli makes section integrals measurable and permits exchange of nonnegative product integrals. Probability measures and probability spaces, The product sigma-algebra and its finite iterates, For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique, Tonelli's theorem for nonnegative measurable functions on a sigma-finite product

[F9]

For a nonnegative random variable $X$ and $a > 0$ , $P (X \geq a) \leq E [X] / a$ . Markov's inequality for random variables

[F10]

For bounded measurable $f$ and posterior $ρ ≪ π$ , $E_{ρ} f \leq K L (ρ ∥ π) + \log E_{π} e^{f}$ . The PAC-Bayes change-of-measure inequality

[F11]

Finite sums, differences, and Borel compositions of measurable real-valued functions are measurable. Arithmetic and lattice operations preserve measurability whenever they are defined, Composition with a Borel measurable outer map preserves measurability

[F12]

The natural logarithm is defined as the inverse of the exponential, is increasing, has $\log 1 = 0$ , and satisfies $\log (x y) = \log x + \log y$ for positive $x, y$ . The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm

[F13]

The one-cell measurable partition contributes $0$ to the finite-partition definition of $K L$ , so $K L (ρ ∥ π) \geq 0$ . PAC-Bayes priors, posteriors, and relative entropy

[F14]

The real exponential is defined on $R$ , positive, and strictly increasing. The real exponential function and the number $e$ by a power series, The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , The exponential function is strictly increasing

Proof

Given: The hypotheses in the Statement.

1.1A1F1F2F3F4F5F6F7F8F12F13givenalgebra

For fixed $θ$ , the map $z \mapsto (θ, z)$ is measurable: the preimage of a generating rectangle $A \times B$ is $B$ if $θ \in A$ , and empty otherwise. Thus $f_{θ} (z) : = ℓ (θ, z)$ is measurable. Apply [F1] to the supervised problem with instance space $Z$ , singleton label space ${*}$ , action space $[0, C]$ with its Borel sigma-algebra, predictor class ${f_{θ}}$ , loss $L (a, *) = a$ , and joint law $D \otimes δ_{*}$ , where $δ_{*} ({*}) = 1$ . Tonelli [F8] identifies its population risk with $R (θ)$ , and its empirical risk on $((Z_{i}, *))_{i = 1}^{m}$ is ${\hat{R}}_{S} (θ)$ . If $C = 0$ , both risks are zero and the bound follows because [F13] gives $K L (ρ ∥ π) \geq 0$ and [F12] gives $\log (1 / δ) > 0$ . Suppose $C > 0$ and put $Y_{i} = ℓ (θ, Z_{i})$ . By [F2]–[F4], the $Y_{i}$ are independent and $E Y_{i} = R (θ)$ . Apply [F6] to $Y_{i} / C \in [0, 1]$ with $t = - λ C / m$ , and use [F5] to rescale the centered variable, obtaining $E \exp (- λ (Y_{i} - R (θ)) / m) \leq \exp (λ^{2} C^{2} / (8 m^{2}))$ . By [F7] and the exponential addition formula, the finite product factors, so $E_{S} \exp (λ (R (θ) - {\hat{R}}_{S} (θ))) \leq \exp (\frac{λ^{2} C^{2}}{8 m})$ .

2.1A1F1F8F11F14step 1.1construct

The fixed-predictor risks are defined by [F1], and the bounded product-measurable loss makes $R (θ)$ measurable in $θ$ by [F8]; finite projection, arithmetic, and Borel composition make $(θ, S) \mapsto \exp (λ (R (θ) - {\hat{R}}_{S} (θ)))$ product-measurable by [F11]. By [F14], this integrand lies between $e^{- λ C} > 0$ and $e^{λ C}$ . Thus $M_{λ} (S) : = E_{θ \sim π} \exp (λ (R (θ) - {\hat{R}}_{S} (θ)))$ is measurable, positive, and Tonelli [F8] exchanges the prior and sample integrals. Integrating step 1.1 over $π$ gives $E_{S} M_{λ} (S) \leq \exp (λ^{2} C^{2} / (8 m))$ .

3.1A1F9F14step 2.1algebra

By [F9] with threshold $\exp (λ^{2} C^{2} / (8 m)) / δ$ , the event $M_{λ} (S) \leq \exp (λ^{2} C^{2} / (8 m)) / δ$ has probability at least $1 - δ$ .

4.1A1F10F12F14step 3.1algebra

On this event, for every posterior $ρ ≪ π$ , apply [F10] to the bounded measurable function $f_{S} (θ) = λ (R (θ) - {\hat{R}}_{S} (θ))$ . This gives $λ (E_{ρ} R - E_{ρ} {\hat{R}}_{S}) \leq K L (ρ ∥ π) + \log M_{λ} (S) \leq K L (ρ ∥ π) + λ^{2} C^{2} / (8 m) + \log (1 / δ)$ by [F12]. Divide by $λ > 0$ ; when the KL value is infinite the inequality is vacuous.

5.1step 1.1step 3.1step 4.1given∎

The event in step 3.1 is independent of $ρ$ , and step 4.1 proves the bound for every posterior on that one event, which has probability at least $1 - δ$ . The $C = 0$ case was handled in step 1.1, so the theorem holds for all $C \geq 0$ .

Remarks

This is a posterior-average risk bound. It does not assert that $R (θ)$ obeys the same inequality for every individual $θ$ sampled from $ρ$ .

Depends on

Used by

A PAC-Bayes bound for a finite tuning grid Corollary
A data-dependent prior can invalidate the PAC-Bayes bound Counterexample
A posterior concentrated on one hypothesis Example

Dependency tree · two levels

101 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, Theorem 2.1 and proof (standard reference, not scraped)