TheoremStatement: 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 posterior mixture of future kernels is a probability kernel

Statement

Let $Π$ be a probability kernel from $(Y, Y)$ to $(Θ, T)$ and let $Q$ be a probability kernel from $(Θ, T)$ to $(Z, Z)$ . For $Q_{y}^{p r e d} (B) = \int_{Θ} Q_{θ} (B) Π_{y} (d θ),$ each $Q_{y}^{p r e d}$ is a probability measure, the evaluations $y \mapsto Q_{y}^{p r e d} (B)$ are measurable, and, for every nonnegative measurable $g : Z \to [0, \infty]$ , $\int_{Z} g (z) Q_{y}^{p r e d} (d z) = \int_{Θ} (\int_{Z} g (z) Q_{θ} (d z)) Π_{y} (d θ) .$

Facts & Assumptions

Given: The probability kernels $Π$ and $Q$ above, and the definition of $Q^{p r e d}$ .

[F1]

The posterior-predictive set function is the stated mixture integral. Posterior-predictive probability kernel

[F2]

A probability kernel has probability-measure sections and measurable event evaluations. Measure kernel and probability kernel

[F3]

A probability measure and parameter-measurable probability kernel define a joint probability measure whose nonnegative integrals are the iterated kernel integrals. A prior and model kernel define a joint law

[F4]

Integrating a nonnegative product-measurable function against a probability kernel gives a measurable function of the kernel index. Measurability of integration against a kernel

Proof

Given: The hypotheses in the Statement.

1.1givenF1F2F3

Fix $y \in Y$ and regard $Π_{y}$ as a probability measure on $Θ$ . By [F2], $Q$ is a probability kernel, so [F3] gives a joint probability measure $J_{y}$ on $Θ \times Z$ satisfying $J_{y} (A \times B) = \int_{A} Q_{θ} (B) Π_{y} (d θ)$ and the iterated-integral identity for every nonnegative product-measurable function. Taking $A = Θ$ shows $Q_{y}^{p r e d} (B) = J_{y} (Θ \times B)$ ; hence it is the second marginal of a probability measure and is itself a probability measure. The same identity applied to $(θ, z) \mapsto g (z)$ gives the displayed integral formula.

2.1givenF1F2F4∎

Fix $B \in Z$ . The function $θ \mapsto Q_{θ} (B)$ is $T$ -measurable by [F2], so $(y, θ) \mapsto Q_{θ} (B)$ is $Y \otimes T$ -measurable as the composition with the measurable coordinate projection. By [F4], $y \mapsto \int_{Θ} Q_{θ} (B) Π_{y} (d θ)$ is measurable. By [F1] this is $Q_{y}^{p r e d} (B)$ , proving kernel measurability.

Depends on

Used by

Posterior-predictive mean and variance decomposition Theorem

Cited to discharge well-definedness by Posterior-predictive probability kernel.

Dependency tree · two levels

17 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

Andrew Gelman et al., Bayesian Data Analysis, 3rd ed., §1.3 (standard reference, not scraped)
Alicia A. Johnson, Miles Q. Ott, and Mine Dogucu, Bayes Rules!, Chapter 8 §8.3 (standard reference, not scraped)