TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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 posterior-risk minimizer minimizes prior risk

Statement

Assume the Axiom of Choice. Let $K$ be a probability kernel from a standard-Borel parameter space $(Θ, T)$ to a standard-Borel data space $(X, A)$ , where standard Borel means measurably isomorphic to a Polish space (Standard Borel spaces). Let $π$ be a prior, and let $L : Θ \times D \to [0, + \infty]$ be jointly measurable for a measurable action space $(D, G)$ . Let $J$ be the joint prior-data law of A prior and model kernel define a joint law, let $M$ be its data marginal, and let $Π_{x} (d θ)$ be a regular posterior distribution of $θ$ given $x$ (the disintegration is supplied by Disintegration of a joint law on standard borel spaces). Define posterior risk $q (x, a) = \int_{Θ} L (θ, a) Π_{x} (d θ) .$ Suppose a measurable deterministic rule $d^{*} : X \to D$ attains the posterior minimum for $M$ -almost every $x$ ; that is, $q (x, d^{*} (x)) \leq q (x, a)$ for every $a \in D$ on one measurable $M$ -full-measure set. Then $d^{*}$ minimizes prior-integrated risk among all randomized decision rules $δ$ : $r_{π} (d^{*}) \leq r_{π} (δ) .$ No conclusion is asserted when a measurable posterior minimizer does not exist. All risks may be $+ \infty$ .

Facts & Assumptions

Given: The kernels, prior, joint loss, posterior, and measurable minimizing rule in the statement.

[A1]

Assume AC, as required by standard-Borel disintegration (The Axiom of Choice).

[F1]

The model is a probability kernel from parameters to data (Parameter-measurable statistical models as kernels).

[F2]

A randomized decision rule is a probability kernel and its risk is the iterated nonnegative loss integral (Randomized procedures as probability kernels, Loss functions and risk).

[F3]

A prior and model kernel define a joint probability whose integral of each nonnegative product-measurable function is the iterated kernel integral (A prior and model kernel define a joint law).

[F4]

On standard-Borel spaces, the joint law disintegrates through its data marginal into a regular posterior, and the integral identity holds for every nonnegative product-measurable function (Regular conditional distribution, Disintegration of a joint law on standard borel spaces).

[F5]

Integrals of nonnegative product-measurable functions against kernels are measurable (Measurability of integration against a kernel).

[F6]

Tonelli's theorem equates iterated integrals of nonnegative measurable functions on product probability spaces (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F7]

The nonnegative integral over a measurable null set is zero (A nonnegative integral over a null set vanishes).

[F8]

The nonnegative integral is monotone (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F9]

The nonnegative integral is additive on finite sums (Additivity of the nonnegative Lebesgue integral).

[F10]

A function between measurable spaces is measurable when preimages of measurable sets are measurable (A measurable function between measurable spaces).

[F11]

Prior-integrated risk is $r_{π} (δ) = \int_{Θ} R (θ, δ) π (d θ)$ (Bayes risk and minimax risk).

[F12]

Product sigma-algebras are generated by measurable rectangles, so coordinate projections and measurable pairing maps into finite products are measurable (The product sigma-algebra and its finite iterates).

Proof

technique · direct

1.1F1F2F3F5F11F12

Fix a randomized rule $δ$ and put $h_{δ} (θ, x) = \int_{D} L (θ, a) δ (x, d a)$ . The lifted kernel $((θ, x), B) \mapsto δ (x, B)$ is a probability kernel because the coordinate projection $(θ, x) \mapsto x$ is measurable by [F12]. The lifted integrand $(θ, x, a) \mapsto L (θ, a)$ is product-measurable because the pairing map $((θ, x), a) \mapsto (θ, a)$ is measurable by [F12]. By [F5], $h_{δ}$ is product-measurable. The risk definition [F2], prior-risk definition [F11], and joint-law identity [F3] therefore give $r_{π} (δ) = \int h_{δ} d J$ .

2.1A1F3F4step 1.1

Apply the posterior disintegration identity [F4] to $h_{δ} \geq 0$ . If $M$ is the second marginal of $J$ , then $r_{π} (δ) = \int_{X} (\int_{Θ} h_{δ} (θ, x) Π_{x} (d θ)) M (d x)$ . Every integral is an extended nonnegative integral, so no integrability beyond the stated measurability is needed.

3.1F2F5F6F12step 2.1

Lift $Π$ to the kernel $((x, a), B) \mapsto Π_{x} (B)$ from $X \times D$ to $Θ$ . The pairing map $((x, a), θ) \mapsto (θ, a)$ is measurable by [F12], so [F5] makes $q (x, a)$ product-measurable. For each fixed $x$ , [F6] applied to the product probability $Π_{x} \times δ (x, \cdot)$ and $L (θ, a)$ gives $\int_{Θ} h_{δ} (θ, x) Π_{x} (d θ) = \int_{D} q (x, a) δ (x, d a)$ . The right side is measurable in $x$ by [F5]. Thus step 2.1 yields $r_{π} (δ) = \int_{X} \int_{D} q (x, a) δ (x, d a) M (d x)$ .

4.1givenF2F5F7F8F9F10F12step 3.1algebra∎

The point-mass kernel $δ^{*} (x, B) = 1_{B} (d^{*} (x))$ is measurable because $d^{*}$ is measurable by [F10]; applying step 3.1 gives $r_{π} (d^{*}) = \int g d M$ for $g (x) = q (x, d^{*} (x))$ . The pairing map $x \mapsto (x, d^{*} (x))$ is measurable by [F10, F12], so $g$ is measurable. Put $h (x) = \int q (x, a) δ (x, d a)$ , which is measurable by [F5]. On the measurable full-measure set $E$ from the statement, $g 1_{E} \leq h 1_{E}$ , so [F8] gives $\int g 1_{E} d M \leq \int h 1_{E} d M$ . The complementary integrals vanish by [F7]; additivity [F9] gives $\int g d M \leq \int h d M = r_{π} (δ)$ by step 3.1. The rule $δ$ was arbitrary.

Depends on

Used by

An open action set need not contain a posterior-risk minimizer Counterexample

Dependency tree · two levels

50 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

Ryan Martin, Lecture Notes on Advanced Statistical Theory, §5.3.1, PDF pp. 104–107 (standard reference, not scraped)
Peter Hoff, Statistical Decision Problems, §§4–5, PDF pp. 7–13 (standard reference, not scraped)