LemmaStatement: AI-adaptedProof: 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 prior and model kernel define a joint law

Statement

Let $(Θ, T)$ and $(X, A)$ be measurable spaces, let $π$ be a probability measure on $(Θ, T)$ , and let $K : Θ \times A \to [0, 1]$ be a probability kernel. For $C \in T \otimes A$ , write $C_{θ} = {x \in X : (θ, x) \in C}$ and set $J (C) = \int_{Θ} K (θ, C_{θ}) π (d θ) .$ Then $J$ is a probability measure on the product sigma-algebra, and for every nonnegative product-measurable $h$ , $\int_{Θ \times X} h (θ, x) J (d θ, d x) = \int_{Θ} (\int_{X} h (θ, x) K (θ, d x)) π (d θ) .$ In particular, $J (A \times B) = \int_{A} K (θ, B) π (d θ)$ for $A \in T$ and $B \in A$ .

Facts & Assumptions

Given: The measurable spaces, prior, and probability kernel in the statement.

[F1]

The parameter-measurable model is a probability kernel, so every section is a probability and every event evaluation is measurable (Parameter-measurable statistical models as kernels).

[F2]

Sections of a product-measurable set are measurable (Every section of a product-measurable function is measurable).

[F3]

Integrating a nonnegative product-measurable function against a kernel gives a measurable function (Measurability of integration against a kernel).

[F4]

Nonnegative functions admit increasing simple approximations and increasing limits pass through integrals (Every nonnegative measurable function is the increasing limit of simple measurable functions, Monotone convergence for the integral).

[F5]

A probability measure has total mass one and is countably additive (Probability measures and probability spaces).

[F6]

The nonnegative integral is additive on finite sums and homogeneous under nonnegative scalars (Additivity of the nonnegative Lebesgue integral, Monotonicity and nonnegative homogeneity of the nonnegative integral).

Proof

technique · direct

1.1F1F2F3F5

For each $C \in T \otimes A$ , [F2] makes $C_{θ}$ measurable and [F3], applied to $1_{C}$ , makes $θ \mapsto K (θ, C_{θ})$ measurable. Thus $J (C)$ is defined. The empty set has $J$ -mass zero, while $(Θ \times X)_{θ} = X$ and [F1], [F5] give $J (Θ \times X) = 1$ .

2.1F1F4F5step 1.1

If $(C_{n})_{n \geq 0}$ are pairwise disjoint product-measurable sets, their sections are pairwise disjoint. Countable additivity of each $K (θ, \cdot)$ gives $K (θ, (⋃_{n} C_{n})_{θ}) = \lim_{N} \sum_{n = 0}^{N} K (θ, (C_{n})_{θ})$ . The partial sums increase; [F4] passes this limit through the $π$ -integral and yields $J (⋃_{n} C_{n}) = \sum_{n} J (C_{n})$ . Therefore $J$ is a probability measure.

3.1F1F3F6step 1.1step 2.1

For a rectangle $A \times B$ , its section is $B$ on $A$ and empty off $A$ , so the definition gives $J (A \times B) = \int_{A} K (θ, B) π (d θ)$ . For a nonnegative simple function $h = \sum_{i = 1}^{m} c_{i} 1_{C_{i}}$ with disjoint measurable sets and $c_{i} \geq 0$ , the set formula for $J$ and [F6] give the displayed iterated-integral identity by finite addition and homogeneity.

4.1F2F3F4step 3.1∎

For general nonnegative product-measurable $h$ , take the increasing simple approximants of [F4]. Apply monotone convergence first under $J$ , then sectionwise under each $K (θ, \cdot)$ , and finally under $π$ . The identity for the simple functions from step 3.1 passes to the limit, including when either side is $+ \infty$ .

Depends on

Used by

Metropolis–Hastings kernel Algorithm
Posterior RCD exists for a standard-Borel parameter Corollary
Approximate Bayesian computation and the tolerance-conditioned target Definition
Augmented ABC tolerance target Definition
Bayesian posterior as a regular conditional law Definition
Finite-group hierarchical Bayesian model Definition
General-state reversibility by symmetric flow measure Definition
Particle Gibbs extended target Definition
A Bayesian posterior RCD indexed by the sample point Example
A finite Bayesian update and a null-data posterior version Example
A symmetric random walk on the circle Example
A systematic Gaussian Gibbs sweep need not be reversible Example
A Gibbs refresh is conditionally independent of the old block Lemma
Each exact Gibbs block update is reversible and invariant Lemma
Gaussian reference-kernel mutual-information lower bound Lemma
The augmented ABC target has the tolerance posterior as its parameter marginal Lemma
The common-density Metropolis–Hastings ratio Lemma
The same-marginal conditional-product law is well-defined Lemma
A finite-group hierarchical model has a conditional law of its latent tuple Theorem
A posterior mixture of future kernels is a probability kernel Theorem
A posterior-risk minimizer minimizes prior risk Theorem
A sufficient summary preserves the Bayesian posterior Theorem
A systematic Gibbs sweep preserves the target Theorem
Current-group and new-group posterior predictions are probability kernels Theorem
Dirichlet-process posterior update Theorem
General-state reversibility implies invariance Theorem
Hierarchical posterior normalization on positive finite evidence Theorem
KL chain rule for standard-Borel disintegrations Theorem
Metropolis–Hastings flow is reversible and invariant Theorem
Sequential ABC Radon–Nikodym weights target each tolerance law Theorem
Standard-Borel Bayesian posterior kernel exists Theorem
The Metropolized Hamiltonian chain preserves its target Theorem

Dependency tree · two levels

34 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.1 and 5.3.1, PDF pp. 100–105 (standard reference, not scraped)
Peter Hoff, Statistical Decision Problems, §§4–5, PDF pp. 7–13 (standard reference, not scraped)