Pipeline-generated

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.

✓ 1 result · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 1 also cleared it.

Posterior propriety and dominated Bayes formula

1 · Prerequisites

2 · Summary

For a fixed observation, the evidence is the integral of the nonnegative likelihood section against the prior measure. The normalized fiberwise update is a probability exactly when this evidence is finite and positive; neither zero nor infinite evidence can be used as a denominator. A sigma-finite improper prior can therefore give a proper posterior at a particular data fiber, but that update does not define a prior-predictive probability. A proper prior is a probability measure, as in Bayesian model as a prior and sampling kernel. The posterior RCD and data-indexed posterior-kernel distinction is stated in Bayesian posterior as a regular conditional law; a fiberwise update alone does not assert either conditional-law identity.

For a proper prior, the general dominated-kernel formula is already proved in Bayes formula for dominated kernels. Its hypotheses include a sigma-finite data measure, a probability sampling kernel, and one specified nonnegative density measurable jointly in parameter and data. Under these hypotheses the normalizer is the prior-predictive density; the quotient formula applies only on fibers with finite positive evidence, and the theorem fills the complement with a probability version on a prior-predictive null set.

The density hypotheses are substantive. Dominated statistical experiments only gives domination of each sampling law by a fixed sigma-finite measure, and Likelihood densities supplies separate parameter-indexed versions without asserting their joint measurability. Do not infer a product-measurable density from those pointwise versions. Supply joint measurability explicitly when using Tonelli for a prior-predictive statement.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Evidence normalizer and fiberwise posterior update

Definition

Let $(Θ, T)$ be a measurable parameter space, let $Π$ be a sigma-finite measure on it, and fix a data value $y$ . Let $L_{y} : Θ \to [0, + \infty]$ be a $T$ -measurable function. Define its evidence normalizer by $Z_{Π} (y) : = \int_{Θ} L_{y} (θ) Π (d θ) \in [0, + \infty] .$ Only when $0 < Z_{Π} (y) < + \infty$ define the fiberwise posterior update by $Π_{y} (A) : = \frac{\int_{A} L_{y} (θ) Π (d θ)}{Z_{Π} (y)} (A \in T) .$ The definition makes no quotient at zero or infinite evidence. A prior is proper when $Π (Θ) = 1$ , as in Bayesian model as a prior and sampling kernel. We call a sigma-finite prior improper when $Π (Θ) = + \infty$ ; the formula also applies to other sigma-finite measures. For an improper prior, $Z_{Π} (y)$ is a fiberwise normalizer only; it does not by itself define a prior-predictive probability or a conditional law.

When the data are described by a dominated experiment, the dominating measure and its sigma-finiteness are as in Dominated statistical experiments. A family of pointwise likelihood sections is not assumed to be jointly measurable in parameter and data; that additional condition must be supplied separately whenever Tonelli is used.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Fiberwise posterior propriety is equivalent to finite positive evidence

Statement

Let $(Θ, T, Π)$ be a measure space, let $L_{y} : Θ \to [0, + \infty]$ be measurable for a fixed datum $y$ , and put $Z : = \int_{Θ} L_{y} d Π$ . For a finite positive constant $c$ , the set function $A ⟼ c \int_{A} L_{y} d Π$ is a probability measure if and only if $0 < Z < + \infty$ and $c = Z^{- 1}$ . In particular, if $Z = 0$ or $Z = + \infty$ , no finite positive scaling makes the fiberwise update a probability measure.

Facts & Assumptions

Given: A measure space $(Θ, T, Π)$ ; a nonnegative measurable likelihood section $L_{y}$ ; its evidence $Z$ ; and a scalar $c \in (0, + \infty)$ .

[F2]

The indefinite integral of a nonnegative measurable function is a measure: for a measure $Π$ and nonnegative measurable $L_{y}$ , the set function $A \mapsto \int_{A} L_{y} d Π$ is a measure.

[F3]

Probability measures and probability spaces: a probability measure is a measure whose total mass is one.

Proof

Given: The hypotheses in the Statement.

1.1givenF2algebra

Define $ν_{y} (A) : = \int_{A} L_{y} d Π$ . By [F2], $ν_{y}$ is a measure and $ν_{y} (Θ) = Z$ by the Statement's definition of $Z$ and the definition of the integral over a measurable set. Since $c$ is finite and positive, $c ν_{y}$ is also a measure and has total mass $c Z$ , with the extended-real convention $c \cdot (+ \infty) = + \infty$ .

2.1step 1.1F3algebra∎

If $0 < Z < + \infty$ , then $c ν_{y}$ is a probability exactly when $c Z = 1$ by [F3], which is equivalent to $c = Z^{- 1}$ . If $Z = 0$ , its total mass is zero; if $Z = + \infty$ , its total mass is infinite. Thus neither endpoint admits such a $c$ , proving both directions without forming a quotient there.

5 · Examples, counterexamples and false statements

None yet.