TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)

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.

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.

Depends on

Used by

Dependency tree · two levels

125 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

M. Dashti and A. M. Stuart, The Bayesian Approach to Inverse Problems (full lecture notes, arXiv:1302.6989) (standard reference, not scraped)
J. Latz, On the Well-posedness of Bayesian Inverse Problems, SIAM/ASA Journal on Uncertainty Quantification 8 (2020) (standard reference, not scraped)