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.

Likelihood potentials and posterior propriety

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Misfit evidence and the potential posterior law

Definition

Let $X$ be a separable real Banach space with its norm topology, $D \subseteq X$ a Borel forward-map domain, and $μ_{0}$ a Borel probability measure on $X$ with $μ_{0} (D) = 1$ . Write $μ_{0, D}$ for its restriction to $D$ , so $μ_{0, D} (A) = μ_{0} (A)$ for $A \in B (D) : = {D \cap B : B \in B (X)}$ . Let $(Y, Y)$ be a measurable data space. A likelihood potential is a function $Φ : D \times Y \to (- \infty, + \infty]$ that is measurable from $(D \times Y, B (D) \otimes Y)$ to $((- \infty, + \infty], B ((- \infty, + \infty]))$ , where $B ((- \infty, + \infty])$ is the trace of $B (\overline{R})$ on $(- \infty, + \infty]$ . Viewing $Φ$ via the inclusion $(- \infty, + \infty] ↪ \overline{R}$ , it is also product-measurable as an extended-real-valued map because for every Borel set $B \subseteq \overline{R}$ , $Φ^{- 1} (B) = Φ^{- 1} (B \cap (- \infty, + \infty])$ is measurable by the definition of the trace sigma-algebra. Here $+ \infty$ is allowed and $- \infty$ is excluded; set $e^{- \infty} = 0$ . The scalar map $t \mapsto e^{- t}$ on this range is continuous at finite $t$ , and is continuous at $+ \infty$ : given $ε > 0$ , the limit supplies $a \in R$ such that $t > a$ implies $e^{- t} < ε$ , and the order-topology neighborhood $(a, + \infty]$ maps into $[0, ε)$ . Hence it is Borel, so $L_{Φ} : D \times Y \to [0, + \infty)$ , $L_{Φ} (u; y) : = e^{- Φ (u; y)}$ , is product-measurable by composition, and each section $u \mapsto L_{Φ} (u; y)$ is nonnegative and measurable. Define its evidence by

Z_{Φ} (y) : = \int_{D} L_{Φ} (u; y) μ_{0, D} (d u) \in [0, + \infty] .

For each fixed $y$ with $0 < Z_{Φ} (y) < + \infty$ , define the normalized fiberwise update on $A \in B (D)$ by $Π^{y} (A) : = \frac{\int_{A} L_{Φ} (u; y) μ_{0, D} (d u)}{Z_{Φ} (y)} .$ No normalized fiberwise update is defined by this formula when $Z_{Φ} (y) = 0$ or $Z_{Φ} (y) = + \infty$ .

For a data-indexed claim, an observation model and its version convention must also be specified. In the dominated case, let $Q$ be a proper probability kernel from $(D, B (D))$ to $(Y, Y)$ , let $ν$ be a sigma-finite measure on $(Y, Y)$ , and suppose $Q (u, B) = \int_{B} L_{Φ} (u; y) ν (d y)$ for every $u \in D$ and $B \in Y$ . Then $Z_{Φ}$ is the density of the prior-predictive data law with respect to $ν$ ; a data-indexed conditional-law version uses $Π^{y}$ when $0 < Z_{Φ} (y) < \infty$ and the prior $μ_{0, D}$ when $Z_{Φ} (y)$ is zero or infinite. These filled fibers have zero prior-predictive mass, and their chosen values are not normalized fiberwise updates. More generally, for a proper Bayesian model with standard-Borel parameter space $(D, B (D))$ and data space $(Y, Y)$ (each measurably isomorphic to the Borel space of a Polish space), the Axiom of Choice guarantees a data-indexed posterior kernel; its values are unique as probability measures outside one data-marginal-null set, and values on that null set remain version choices. The dominated construction is choice-free; the separate standard-Borel existence branch assumes the Axiom of Choice.

Definition references

A prior on the admissible domain is a Borel probability with full mass there, and its restriction is a probability.

A measurable space consists of a set and a sigma-algebra.

Joint measurability uses the product sigma-algebra.

The potential takes extended real values, allows positive infinity, and excludes negative infinity.

The extended real line carries its order-topology Borel sigma-algebra.

A function is measurable when preimages of measurable target sets are measurable in the source.

Every section of a product-measurable extended-real function is measurable.

Composing a measurable map with a Borel outer map preserves measurability.

The real exponential is continuous on finite inputs.

The exponential tends to zero at negative infinity, giving the likelihood map's value zero at positive infinity.

A continuous scalar map has Borel preimages of Borel sets.

A proper Bayesian model is a probability prior with a parameter-measurable probability sampling kernel.

A probability kernel has measurable evaluations and probability sections at every parameter.

The dominating data measure is sigma-finite.

Fixed-data evidence normalizers are defined for sigma-finite priors, but do not define a prior-predictive law for an improper prior.

A nonnegative likelihood update is a probability exactly when its evidence is positive and finite and the scale is the reciprocal.

A jointly measurable dominated sampling density gives the prior-predictive density and a conditional kernel with prior fillers on zero and infinite fibers.

A posterior RCD is sample-point-indexed; a data-indexed posterior kernel is a version and its null-set values are not fixed.

Changing a conditional kernel on a measurable data-marginal-null set preserves its conditional identities.

Standard Borel means measurably isomorphic to a Polish space with its Borel sigma-algebra.

The Axiom of Choice states that every family of nonempty sets has a choice function.

Under AC and standard-Borel parameter and data spaces, a data-indexed posterior kernel exists and is unique off one data-marginal-null set.

Dashti and Stuart, §3.2 and §4.1, full lecture notes

Latz, §2.2, Theorem 2.5 and its proof in Appendix B (printed p. 23), full paper

TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Function-space posterior propriety from a common lower envelope

Statement

Let $X$ be a separable real Banach space with norm $∥ \cdot ∥_{X}$ , let $D \subseteq X$ be Borel, and let $μ_{0}$ be a Borel probability on $X$ with $μ_{0} (D) = 1$ . Here $B (X)$ is generated by the norm-open sets. Give $D$ the relative topology and Borel sigma-algebra $B (D) = {D \cap B : B \in B (X)}$ , and let $μ_{0, D}$ be the restriction of $μ_{0}$ to $D$ , so $μ_{0, D} (A) = μ_{0} (A)$ for $A \in B (D)$ . Let $(Y, Y)$ be a measurable data space. Assume $Φ : D \times Y \to (- \infty, + \infty]$ is measurable from $(D \times Y, B (D) \otimes Y)$ to $((- \infty, + \infty], B ((- \infty, + \infty]))$ , where $B (\overline{R})$ is generated by the order topology on the extended real line and $B ((- \infty, + \infty])$ is its trace on $(- \infty, + \infty]$ ; thus $+ \infty$ is allowed and $- \infty$ is excluded. Let $Y_{0} \subseteq Y$ . Suppose that for every $y \in Y_{0}$ , the section $u \mapsto Φ (u; y)$ is finite and continuous as a real-valued function on $D$ with its relative topology inherited from the norm topology. Suppose there is one Borel function $M_{1} : [0, \infty) \to [0, \infty)$ , independent of $y \in Y_{0}$ , such that $Φ (u; y) \geq - M_{1} (∥ u ∥_{X}) (u \in D, y \in Y_{0}), \int_{D} e^{M_{1} (∥ u ∥_{X})} μ_{0, D} (d u) < \infty .$ Define $supp μ_{0} : = {x \in X : μ_{0} (U) > 0 for every open neighborhood U of x}$ . Then for every $y \in Y_{0}$ , the evidence $Z_{Φ} (y)$ is finite and strictly positive, and the normalized fiberwise update $Π^{y}$ is a probability measure on $D$ .

Statement references

The evidence and normalized fiberwise update are defined only by the displayed likelihood potential and its fixed-data normalizer.

A prior is a Borel probability on the parameter space with full measure on the forward domain.

A separable space has an at most countable dense subset.

A nonnegative likelihood update is a probability exactly when its normalizer is positive and finite.

Dashti and Stuart, §3.2 and §4.1, full lecture notes

Latz, §2.2, Theorem 2.5 and its proof in Appendix B (printed p. 23), full paper

Facts & Assumptions

Given: A separable real Banach space $X$ , a Borel set $D \subseteq X$ , a Borel probability $μ_{0}$ with $μ_{0} (D) = 1$ , a jointly measurable potential $Φ$ with finite continuous sections on $D$ for $y \in Y_{0}$ , and one common envelope $M_{1}$ satisfying the stated integrability condition.

[F1]

A prior on a forward domain is a Borel probability $μ_{0}$ on $X$ with $μ_{0} (D) = 1$ , and its restriction $μ_{0, D}$ is a probability on $D$ . A Borel prior concentrated on a forward-map domain

[F2]

For a fixed $y$ , $Z_{Φ} (y) = \int_{D} e^{- Φ (u; y)} μ_{0, D} (d u)$ and, only for positive finite evidence, $Π^{y} (A) = Z_{Φ} (y)^{- 1} \int_{A} e^{- Φ (u; y)} μ_{0, D} (d u)$ . Misfit evidence and the potential posterior law

[F3]

Separability means that some at most countable subset is dense. Separability: the existence of an at most countable dense subset

[F4]

A product of two at most countable sets is at most countable. A product of two at most countable sets is at most countable

[F5]

The rational numbers are countably infinite. $Q$ is countably infinite

[F6]

Between any two distinct reals lies a rational. Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable

[F7]

The Borel sigma-algebra is generated by the open sets. The Borel sigma-algebra of a topological space

[F8]

A measure of a countable union is at most the sum of the measures of its members. Finite and countable subadditivity of measures

[F9]

If measurable sets satisfy $A \subseteq B$ , then $μ (A) \leq μ (B)$ . Measures are monotone

[F10]

For nonnegative measurable functions, pointwise domination implies domination of their nonnegative integrals. Monotonicity and nonnegative homogeneity of the nonnegative integral

[F11]

For a measure $μ$ and nonnegative measurable likelihood $L_{y}$ , the normalized update $A \mapsto Z^{- 1} \int_{A} L_{y} d μ$ is a probability measure exactly when $0 < Z < \infty$ . Fiberwise posterior propriety is equivalent to finite positive evidence

[F12]

A measure assigns zero mass to the empty set. Measures on sigma-algebras

[F13]

A measure is countably additive on pairwise-disjoint measurable sequences. Measures on sigma-algebras

[F14]

A real Banach space is a real normed space with induced metric $d_{X} (x, x^{'}) = ∥ x - x^{'} ∥_{X}$ , complete for that metric. Banach space

[F15]

The norm satisfies $∥ u + v ∥_{X} \leq ∥ u ∥_{X} + ∥ v ∥_{X}$ . A norm on a real vector space, the induced metric, and the dictionary with the metric axioms

[F16]

The open metric ball is $B (x, r) = {z : d_{X} (x, z) < r}$ for $r > 0$ . Open ball, closed ball and sphere in a metric space

[F17]

Every positive-radius open metric ball is open in the metric topology. Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed

[F18]

The open sets of $D$ with the relative topology are precisely traces $U \cap D$ of open sets $U$ in $X$ . Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace

[F19]

The metric topology is the collection of open sets for the metric induced by the norm. The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement

[F20]

Continuity at a point means that the preimage of each target neighborhood is a neighborhood of that point. Continuity of a map of topological spaces at a point and globally

[F21]

The real exponential is continuous, positive and increasing. The real exponential function and the number $e$ by a power series, The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , The exponential function is strictly increasing

[F22]

A nonempty at most countable set is the surjective image of $N$ . A nonempty set is at most countable iff it is a surjective image of $N$

[F23]

Every subset of an at most countable set is at most countable. Every subset of an at most countable set is at most countable

[F24]

The norm triangle inequality gives $∥ u ∥_{X} - ∥ v ∥_{X} \leq ∥ u - v ∥_{X}$ and the reverse inequality after swapping $u, v$ , so $u \mapsto ∥ u ∥_{X}$ is continuous; composing measurable maps with Borel maps preserves measurability. A norm on a real vector space, the induced metric, and the dictionary with the metric axioms, Composition with a Borel measurable outer map preserves measurability

Proof

Given: The hypotheses in the Statement.

1.1givenF3F4F5F6F14F15F16F17F19F22F23chooseconstruct

Choose a countable dense set $C \subseteq X$ using separability [F3]. The positive rationals $Q_{> 0}$ are at most countable by [F5] and [F23], so $C \times Q_{> 0}$ is at most countable by [F4]. It is nonempty because $X$ is a nonempty vector space, $C$ is dense, and $1 \in Q_{> 0}$ . By [F22], enumerate $C \times Q_{> 0}$ by a surjection from $N$ ; composing that map with $(c, q) \mapsto B (c, q)$ shows that $B_{0} : = {B (c, q) : c \in C, q \in Q_{> 0}}$ is at most countable. It consists of open sets by [F17], and it is a base: if $x \in U$ with $U$ open, choose $r > 0$ with $B (x, r) \subseteq U$ , choose $c \in C$ with $d : = ∥ x - c ∥_{X} < r / 3$ , so $d < r - d$ , and then choose a rational $q$ with $d < q < r - d$ by [F6]. The norm triangle inequality [F15] gives $x \in B (c, q) \subseteq B (x, r) \subseteq U$ .

1.2F2F7F10F18F20F21F24givenalgebra

Fix any $y \in Y_{0}$ . The section $Φ (\cdot; y)$ is continuous and real-valued on $D$ , so its preimages of open subsets of $R$ are relatively open by [F18, F20] and hence Borel by [F7]. Since the exponential is continuous [F21], $e^{- Φ (\cdot; y)}$ is Borel measurable. By [F24], $u \mapsto e^{M_{1} (∥ u ∥_{X})}$ is also measurable. The common lower envelope and monotonicity of the exponential [F21] give $0 \leq e^{- Φ (u; y)} \leq e^{M_{1} (∥ u ∥_{X})}$ for every $u \in D$ . Thus [F10] and the assumed envelope integrability give $Z_{Φ} (y) \leq \int_{D} e^{M_{1} (∥ u ∥_{X})} μ_{0, D} (d u) < \infty$ . Since $y$ was arbitrary, this holds for every $y \in Y_{0}$ .

2.1F7F8F9F12F17F22F23step 1.1construct

Let $N : = {B \in B_{0} : μ_{0} (B) = 0}$ and $N : = ⋃ N$ . By [F23], $N$ is at most countable. If $N = \emptyset$ , then $N = \emptyset$ and $μ_{0} (N) = 0$ by [F12]. Otherwise [F22] gives a surjection $b : N \to N$ ; each $b_{n}$ is Borel by [F7] and [F17] and has measure zero, so [F8] gives $μ_{0} (N) = μ_{0} (⋃_{n} b_{n}) \leq \sum_{n} μ_{0} (b_{n}) = 0$ . If $x \notin N$ and $U$ is an open neighborhood of $x$ , the base property supplies $B \in B_{0}$ with $x \in B \subseteq U$ ; then $μ_{0} (B) > 0$ , and [F9] gives $μ_{0} (U) \geq μ_{0} (B) > 0$ . A point in $N$ lies in a zero-mass open neighborhood. Therefore $X ∖ N = supp μ_{0}$ and $μ_{0} (supp μ_{0}) = 1$ .

3.1F1F8F12F13step 2.1choose

Since $μ_{0}$ is a probability and $μ_{0} (D) = 1$ , countable additivity [F13] on $X = D ⊔ (X ∖ D)$ gives $μ_{0} (X ∖ D) = 0$ . Likewise, $μ_{0} (supp μ_{0}) = 1$ by step 2.1 and $μ_{0} (X) = 1$ , so [F13] on the support and its complement gives $μ_{0} (X ∖ supp μ_{0}) = 0$ . By [F8] their union is null, so $μ_{0} (D \cap supp μ_{0}) = 1$ . This intersection is nonempty because [F12] gives $μ_{0} (\emptyset) = 0$ . Choose $x \in D \cap supp μ_{0}$ .

4.1F1F2F10F13F18F20step 3.1givenchoosealgebra

Fix $y \in Y_{0}$ . The open interval $(- \infty, Φ (x; y) + 1)$ contains $Φ (x; y)$ ; continuity at $x$ [F20] gives a relative-open neighborhood $W$ mapped into this interval. By [F18], write $W = U \cap D$ for an open $U \subseteq X$ containing $x$ . Thus $Φ (u; y) \leq Φ (x; y) + 1$ on $W$ . By the support property $μ_{0} (U) > 0$ . Since $U ∖ D \subseteq X ∖ D$ and step 3.1 gives $μ_{0} (X ∖ D) = 0$ , [F9] gives $μ_{0} (U ∖ D) = 0$ ; countable additivity [F13] on $U = W ⊔ (U ∖ D)$ yields $μ_{0, D} (W) = μ_{0} (U) > 0$ . On $W$ , $e^{- Φ (u; y)} \geq e^{- Φ (x; y) - 1}$ . Therefore monotonicity and positive scalar homogeneity of the nonnegative integral [F10] give $Z_{Φ} (y) = \int_{D} e^{- Φ (u; y)} μ_{0, D} (d u) \geq \int_{W} e^{- Φ (u; y)} μ_{0, D} (d u) \geq e^{- Φ (x; y) - 1} μ_{0, D} (W) > 0$ .

5.1F2F11step 1.2step 4.1given∎

For the arbitrary $y$ fixed in step 4.1, steps 1.2 and 4.1 give $0 < Z_{Φ} (y) < \infty$ . Applying [F11] to the measurable likelihood section $e^{- Φ (\cdot; y)}$ shows that the normalized update $Π^{y}$ is a probability measure on $D$ . Since $y \in Y_{0}$ was arbitrary, this holds for every such datum.

4 · Examples, counterexamples and false statements

None yet.