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

A PAC-Bayes bound for a finite tuning grid

Statement

Let $(Θ, A, π)$ and $(Z, B, D)$ be probability spaces. Let $C \geq 0$ , and let $ℓ : Θ \times Z \to [0, C]$ be $A \otimes B$ -measurable. Draw $S = (Z_{1}, \dots, Z_{m})$ from the product law $D^{m}$ , where $m \geq 1$ , and define $R (θ) = \int ℓ (θ, z) D (d z)$ and ${\hat{R}}_{S} (θ) = m^{- 1} \sum_{i = 1}^{m} ℓ (θ, Z_{i})$ . Fix $π$ independently of $S$ and define $K L (ρ ∥ π)$ as the supremum of $\sum_{A \in P} ρ (A) \log (ρ (A) / π (A))$ over finite measurable partitions $P$ of $Θ$ , with zero-numerator terms equal to $0$ and positive-numerator/zero-denominator terms equal to $+ \infty$ . Let $Λ = {λ_{1}, \dots, λ_{N}} \subset (0, \infty)$ be a nonempty finite set fixed independently of the sample. For every $δ \in (0, 1)$ , with probability at least $1 - δ$ over the sample, simultaneously for every probability measure $ρ$ satisfying $π (A) = 0 \Rightarrow ρ (A) = 0$ for each $A \in A$ and every $λ \in Λ$ , $E_{θ \sim ρ} R (θ) \leq E_{θ \sim ρ} {\hat{R}}_{S} (θ) + \frac{λ C^{2}}{8 m} + \frac{K L (ρ ∥ π) + \log (N / δ)}{λ} .$

Statement references

The PAC-Bayes KL generalization bound: for each fixed $λ$ and confidence value, one event controls every posterior average.

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

PAC-Bayes priors, posteriors, and relative entropy: a posterior is a probability measure absolutely continuous with respect to the sample-independent prior; relative entropy is the supremum over finite measurable partitions.

Alquier, User-friendly Introduction to PAC-Bayes Bounds, Chapter 2, Theorem 2.4 and proof: applies a union bound over a finite, sample-independent tuning grid.

Facts & Assumptions

Given: The hypotheses of the PAC-Bayes KL theorem, a nonempty finite grid $Λ$ fixed independently of the sample, and $δ \in (0, 1)$ .

[F1]

For each fixed $λ > 0$ and confidence $η \in (0, 1)$ , with probability at least $1 - η$ , the PAC-Bayes KL inequality holds simultaneously for all posterior probabilities. The PAC-Bayes KL generalization bound

[F2]

The probability of a finite union is at most the sum of the probabilities. Basic identities for a probability measure

[F3]

The natural logarithm is defined on positive reals, is increasing, 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

Proof

Given: The hypotheses in the Statement.

1.1givenF1F3algebra

For each $λ \in Λ$ , apply [F1] with confidence $η = δ / N$ . Its event has probability at least $1 - δ / N$ , and on it every posterior satisfies the bound with $\log (1 / η) = \log (N / δ)$ by [F3].

2.1F1F2step 1.1algebra∎

The intersection of these $N$ events has probability at least $1 - N (δ / N) = 1 - δ$ by [F2]. On that single event the inequality holds for every $λ \in Λ$ and every posterior, which is the claim.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

33 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.4 and proof (standard reference, not scraped)