TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 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.

Gaussian posterior small-ball ratios and the Onsager–Machlup functional

Statement

Assume the Axiom of Choice, the Hahn–Banach theorem, and countable choice. Let $B$ be a real separable Banach space, and let $W$ be a centered Borel Gaussian random element in $B$ with law $μ$ . Define its covariance by $C ℓ = E [ℓ (W) W]$ for $ℓ \in B^{*}$ , let $N = {ℓ : E [ℓ (W)^{2}] = 0}$ , and let $E$ be the completion of $B^{*} / N$ with inner product $⟨ [ℓ], [m] ⟩_{E} = E [ℓ (W) m (W)]$ . Write $i : E \to B$ for the canonical injection extending $[ℓ] \mapsto C ℓ$ . Under AC, the image of the closed $E$ -unit ball is compact in the $B$ norm. Let $Φ : B \to R$ be Borel measurable, locally bounded above, and locally Lipschitz. Suppose that for every $ε > 0$ there is $M_{ε} \in R$ such that $Φ (u) \geq M_{ε} - ε ∥ u ∥_{B}^{2} (u \in B) .$ Define the evidence $Z = \int_{B} e^{- Φ (u)} μ (d u)$ and, when $0 < Z < \infty$ , the posterior $Π (d u) = Z^{- 1} e^{- Φ (u)} μ (d u)$ . Then $0 < Z < \infty$ . For $h \in E$ , define $I (i h) = Φ (i h) + \frac{1}{2} ∥ h ∥_{E}^{2}, I (u) = + \infty (u \notin i E) .$ The functional $I$ attains a finite minimum on $i E$ , and for every fixed $h_{1}, h_{2} \in E$ , $\frac{Π ({\overline{B}}_{B} (i h_{1}, r))}{Π ({\overline{B}}_{B} (i h_{2}, r))} ⟶ \exp ⁣ (I (i h_{2}) - I (i h_{1})) (r ↓ 0) .$ Its minimizers are exactly the Cameron–Martin ratio modes. This pairwise result makes no claim of a global strong small-ball MAP.

Statement references

a Borel probability prior is concentrated on its declared forward domain

the fixed-data posterior is the normalized potential-weighted prior

strong small-ball MAP and Cameron–Martin ratio-mode conventions

the Cameron–Martin norm and canonical injection

Facts & Assumptions

Given: AC, HB, countable choice, a real separable Banach space $B$ , a centered Borel Gaussian random element $W$ with law $μ$ and Cameron–Martin space $E$ , and a Borel locally bounded-above locally Lipschitz potential $Φ$ satisfying the displayed lower bound.

[A1]

AC is required by the Gaussian, Cameron–Martin support, compactness, and Fernique interfaces used here. The Axiom of Choice

[A2]

HB and countable choice are assumed by the finite-projection Gaussian ratio result. The real dominated-extension principle as an additional hypothesis over ZF, The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F1]

A prior is a Borel probability with full mass on its declared domain; the fixed-data posterior is the normalized measure with density proportional to $e^{- Φ}$ on that domain. We specialize to $D = B$ . A Borel prior concentrated on a forward-map domain, Misfit evidence and the potential posterior law

[F2]

If a finite continuous potential on a Borel-prior domain has a common integrable lower envelope, then its evidence is finite and positive and the normalized update is a probability. Function-space posterior propriety from a common lower envelope

[F3]

For some $a > 0$ , $\int_{B} e^{a ∥ u ∥_{B}^{2}} μ (d u) < \infty$ . Fernique integrability for a separable Banach Gaussian law

[F4]

Since $B$ is Polish and $μ$ is a Borel probability, it is tight; the support theorem then gives $supp μ = \overline{i E}$ , so $0$ is a support point. Polish spaces are separable completely metrizable spaces, Every borel probability on a polish space is tight, The support of a Banach Gaussian is the closure of its RKHS

[F5]

The Cameron–Martin space is a Hilbert completion with continuous canonical injection and $ℓ (i h) = ⟨ h, [ℓ] ⟩_{E}$ for $ℓ \in B^{*}$ . Covariance operator and reproducing-kernel Hilbert space of a Banach Gaussian, The Banach Gaussian covariance and RKHS construction is well-defined

[F6]

The closed unit ball of $E$ has compact image in $B$ . The Cameron–Martin unit ball is compact in the Banach norm

[F7]

The Gaussian prior's fixed-center ball ratios converge to $\exp ((∥ h_{2} ∥_{E}^{2} - ∥ h_{1} ∥_{E}^{2}) / 2)$ . Small-ball ratios for Cameron–Martin translates of a Banach Gaussian

[F8]

A Cameron–Martin ratio mode compares every fixed pair of Cameron–Martin ball probabilities by a limit at least $1$ . Small-ball MAP conventions and Cameron–Martin relative modes

[F9]

Every bounded sequence of real numbers has a convergent subsequence. Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence

Proof

technique · establish posterior propriety using Fernique's exponential-square moment, transfer the Gaussian ball-ratio limit through the locally Lipschitz likelihood, and apply the direct method using the compact Cameron–Martin unit ball

1.1A1F1F2F3givenconstruct

Choose $0 < ε < a$ with $a$ from [F3]. The lower bound gives $Φ (u) \geq M_{ε} - ε ∥ u ∥_{B}^{2}$ . Define the nonnegative Borel function $M_{1} (t) = \max {0, ε t^{2} - M_{ε}}$ . Then $Φ (u) \geq - M_{1} (∥ u ∥_{B})$ and $e^{M_{1} (∥ u ∥_{B})} \leq 1 + e^{- M_{ε}} e^{ε ∥ u ∥_{B}^{2}} .$ The right side is $μ$ -integrable by [F3]. Since $Φ$ is locally Lipschitz it is finite and continuous on $B$ . Apply [F2] with the single datum and $D = B$ ; the prior definition in [F1] makes $μ$ a prior on $B$ . Thus $0 < Z < \infty$ and $Π$ is a probability.

1.2F5givenchoosealgebra

Let $C_{i} = ∥ i : E \to B ∥$ . If $E = {0}$ , $I$ has the sole candidate $0$ and is minimized there. Otherwise $C_{i} > 0$ . Choose $ε < 1 / (4 C_{i}^{2})$ and use the potential lower bound to obtain, for every $h \in E$ , $I (i h) \geq M_{ε} + \frac{1}{2} ∥ h ∥_{E}^{2} - ε ∥ i h ∥_{B}^{2} \geq M_{ε} + \frac{1}{4} ∥ h ∥_{E}^{2} .$ Since $I (0) = Φ (0)$ is finite, $\inf_{E} I$ is finite and any minimizing sequence is bounded in $E$ .

2.1A2F1F4F7givenstep 1.1algebra

Fix $h \in E$ . Local Lipschitz continuity at $i h$ supplies constants $L_{h} < \infty$ and $ρ_{h} > 0$ such that $∣ Φ (u) - Φ (i h) ∣ \leq L_{h} r$ whenever $∥ u - i h ∥_{B} \leq r < ρ_{h}$ . Therefore $e^{- Φ (i h) - L_{h} r} μ ({\overline{B}}_{B} (i h, r)) \leq \int_{{\overline{B}}_{B} (i h, r)} e^{- Φ (u)} μ (d u) \leq e^{- Φ (i h) + L_{h} r} μ ({\overline{B}}_{B} (i h, r)) .$ For fixed $h_{1}, h_{2} \in E$ , divide the two integral bounds and cancel the common normalizer $Z$ in [F1]. The factors from the Lipschitz errors tend to $1$ , and [F7] gives $\frac{Π ({\overline{B}}_{B} (i h_{1}, r))}{Π ({\overline{B}}_{B} (i h_{2}, r))} ⟶ e^{Φ (i h_{2}) - Φ (i h_{1})} e^{(∥ h_{2} ∥_{E}^{2} - ∥ h_{1} ∥_{E}^{2}) / 2} = e^{I (i h_{2}) - I (i h_{1})} .$ The denominator is positive for small $r$ : [F4] gives positive prior mass to every open ball about $i h_{2}$ (since $i h_{2} \in i E$ ), and the likelihood is strictly positive and continuous there.

2.2F5F6F9step 1.2givenchoosealgebra

Choose a minimizing sequence $(h_{n})$ in $E$ and, by [F9], pass to a subsequence for which $∥ h_{n} ∥_{E} \to L$ . Its images lie in a fixed multiple of the closed $E$ -unit ball, whose image is compact in $B$ by [F6]. Pass to a further subsequence with $i h_{n} \to v$ in $B$ ; compactness means $v = i h$ for some $h \in E$ . For each $ℓ \in B^{*}$ , [F5] gives $∣ ℓ (i h) ∣ = \lim_{n} ∣ ℓ (i h_{n}) ∣ = \lim_{n} ∣ ⟨ h_{n}, [ℓ] ⟩_{E} ∣ \leq L ∥ [ℓ] ∥_{E} .$ The classes $[ℓ]$ are dense in $E$ by [F5]. For every unit $g \in E$ , choose nonzero classes $[ℓ_{n}] \to g$ and normalize them; then $[ℓ_{n}] / ∥ [ℓ_{n}] ∥_{E} \to g$ . Thus the normalized covariance classes are dense in the unit sphere, and the supremum of $∣ ⟨ h, [ℓ] ⟩_{E} ∣$ over them is $∥ h ∥_{E}$ . The displayed bound gives $∥ h ∥_{E} \leq L$ . Local Lipschitz continuity gives $Φ (i h_{n}) \to Φ (i h)$ , and therefore $I (i h) \leq \lim_{n} (Φ (i h_{n}) + \frac{1}{2} ∥ h_{n} ∥_{E}^{2}) = \inf_{E} I .$ Thus $I$ attains its finite minimum.

3.1F7F8step 2.1step 2.2givenalgebra∎

By [F7], the posterior ball ratio for fixed $i h, i k \in i E$ is $e^{I (i k) - I (i h)}$ . This limit is at least $1$ for every $k \in E$ exactly when $I (i h) \leq I (i k)$ for every $k \in E$ . By [F8], those points are precisely the Cameron–Martin ratio modes. The comparison is only over fixed centers in $i E$ ; no supremum over all $B$ centers has been controlled, so it does not establish a global strong small-ball MAP.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

107 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, K. J. H. Law, A. M. Stuart, and J. Voss, MAP Estimators and Their Consistency in Bayesian Nonparametric Inverse Problems (standard reference, not scraped)
H. Kekkonen and Y. Korolev, Inverse Problems, lecture notes (standard reference, not scraped)