PropositionStatement: 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.

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.

Depends on

Used by

Dependency tree · two levels

12 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

Gelman et al., Bayesian Data Analysis, 3rd ed., §§1.3, 2.8 (standard reference, not scraped)
Johnson, Ott & Dogucu, Bayes Rules!, Chapter 2 (standard reference, not scraped)