TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck passjudge 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 conditional Bayes rule minimizes population risk

Statement

Assume the Axiom of Choice. Let $(X, Σ_{X})$ and $(Y, Σ_{Y})$ be standard Borel spaces, let $(A, Σ_{A})$ be a measurable action space, and let $P$ be a probability measure on $X \times Y$ . Write $P_{X}$ and $P_{Y}$ for its coordinate marginals. There are regular conditional probability kernels $Q (y, d x)$ for $X$ given $Y$ and $K (x, d y)$ for $Y$ given $X$ , with $P (C \times D) = \int_{D} Q (y, C) P_{Y} (d y) = \int_{C} K (x, D) P_{X} (d x) (C \in Σ_{X}, D \in Σ_{Y}) .$ Let $ℓ : A \times Y \to [0, + \infty]$ be measurable with respect to $Σ_{A} \otimes Σ_{Y}$ and define $q (x, a) : = \int_{Y} ℓ (a, y) K (x, d y)$ . If a measurable predictor $f^{*} : X \to A$ has a measurable set $E \in Σ_{X}$ with $P_{X} (E) = 1$ such that $q (x, f^{*} (x)) \leq q (x, a)$ for every $x \in E$ and every $a \in A$ , then $R_{P} (f^{*}) \leq R_{P} (g)$ for every measurable predictor $g : X \to A$ . All risks may be $+ \infty$ .

Statement references

Standard Borel spaces: a standard Borel space is measurably isomorphic to a Polish space.

Regular conditional distribution: a regular conditional distribution is an everywhere probability kernel satisfying the conditional-event integral identities.

The product sigma-algebra and its finite iterates: product sigma-algebras are generated by measurable rectangles.

The Axiom of Choice: AC asserts that every family of nonempty sets has a choice function.

Facts & Assumptions

Given: AC; standard Borel instance and label spaces; a joint probability law $P$ ; a measurable action space; a nonnegative product-measurable loss; and a measurable predictor $f^{*}$ that minimizes conditional risk on one measurable $P_{X}$ -full-measure set.

[A1]

Assume the Axiom of Choice. The Axiom of Choice

[F1]

A standard Borel space is measurably isomorphic to a Polish space. Standard Borel spaces

[F2]

Under AC, a joint law on a product of standard Borel spaces admits a probability kernel in either coordinate direction with the rectangle disintegration identity. Disintegration of a joint law on standard borel spaces

[F3]

The disintegration identity also holds for every nonnegative product-measurable integrand, including value infinity. Disintegration of a joint law on standard borel spaces

[F4]

Under AC and standard Borel parameter/data hypotheses, a measurable rule attaining posterior minimum almost everywhere minimizes prior-integrated risk among all randomized rules. A posterior-risk minimizer minimizes prior risk

[F5]

Population risk is the extended nonnegative integral of the loss under the joint law. Population and empirical risk

[F6]

A regular conditional distribution is a probability kernel whose evaluations satisfy the conditional-event integral identity. Regular conditional distribution

[F7]

Integrating a nonnegative product-measurable function against a probability kernel gives a measurable extended-valued function. Measurability of integration against a kernel

[F8]

Product sigma-algebras are generated by measurable rectangles, so the coordinate swap between finite products is measurable. The product sigma-algebra and its finite iterates

[F9]

A map is measurable when preimages of measurable sets are measurable; this criterion is preserved by composition. A measurable function between measurable spaces

Proof

1.1A1F1F2F6F7F8F9

The spaces satisfy the standard-Borel hypothesis [F1]. Apply [F2] to $P$ and to its coordinate swap. This gives $Q (y, d x)$ and $K (x, d y)$ with the two displayed disintegrations; [F6] identifies them as regular conditional distributions. With prior $π = P_{Y}$ and sampling kernel $Q$ , the joint prior-data law is $P$ and the posterior is $K$ . The loss $L (y, a) : = ℓ (a, y)$ is jointly measurable because the coordinate swap on product spaces has rectangle preimages that are rectangles by [F8], and composition preserves measurability by [F9]. The lifted kernel $\tilde{K} ((x, a), D) : = K (x, D)$ is a probability kernel, since its evaluations are measurable by projection from $x$ ; [F7] therefore makes $q (x, a)$ measurable.

2.1A1F3F4F5F8F9givenstep 1.1algebra∎

For any measurable $g : X \to A$ , the point-mass rule $δ_{g} (x, B) : = 1_{B} (g (x))$ is a probability kernel, since each section is a Dirac probability measure and each evaluation is measurable by [F9]. The function $(y, x) \mapsto ℓ (g (x), y)$ is product-measurable by the rectangle-preimage criterion [F8, F9]. Its prior-integrated risk is $\int_{Y} \int_{X} ℓ (g (x), y) Q (y, d x) P_{Y} (d y) = R_{P} (g)$ by [F3, F5], with the same identity for $f^{*}$ . Under [F4], use parameter $y$ , prior $P_{Y}$ , data $x$ , model kernel $Q$ , posterior $K$ , action space $A$ , loss $L$ , and rule $f^{*}$ . Its posterior risk is $q$ , so the common full-measure minimizing premise applies; the theorem gives prior risk of $f^{*}$ no larger than that of $δ_{g}$ . Thus $R_{P} (f^{*}) \leq R_{P} (g)$ . Since $g$ was arbitrary, the claim follows.

Depends on

Used by

Bayes predictors and excess risk Definition

Dependency tree · two levels

41 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

Shai Shalev-Shwartz and Shai Ben-David, Understanding Machine Learning: From Theory to Algorithms, Chapter 3 §3.2 (standard reference, not scraped)
Mehryar Mohri, Afshin Rostamizadeh, and Ameet Talwalkar, Foundations of Machine Learning, 2nd ed., Chapter 2 §2.4.2 (standard reference, not scraped)