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.

pCN stationary mean acceptance tends to one at small scale

Statement

Assume the Axiom of Choice. Let $H$ be a separable real Hilbert space and let $μ_{0}$ be a centered Borel Gaussian probability measure on $H$ . Let $Φ : H \to [0, \infty)$ be finite-valued and Borel measurable. Suppose that there are constants $p, K > 0$ such that $0 \leq Φ (u) \leq K (1 + ∥ u ∥^{p}) (u \in H),$ and for every $R > 0$ there is a finite $L_{R}$ such that $∣ Φ (u) - Φ (v) ∣ \leq L_{R} ∥ u - v ∥ whenever \max {∥ u ∥, ∥ v ∥} < R .$ Set $Z = \int_{H} e^{- Φ (u)} μ_{0} (d u)$ and $μ (d u) = Z^{- 1} e^{- Φ (u)} μ_{0} (d u)$ . For $β \in [0, 1]$ , let $U \sim μ$ and $ξ \sim μ_{0}$ be independent, put $V_{β} = \sqrt{1 - β^{2}} U + β ξ$ , and define $α_{β} = \min {1, \exp (Φ (U) - Φ (V_{β}))} .$ Then $0 < Z < \infty$ , $μ$ is a probability measure, and the stationary mean acceptance satisfies $\lim_{β ↓ 0} E [α_{β}] = 1.$

Statement references

The pCN proposal combines the current state with an independent Gaussian reference draw and accepts by the potential ratio.

A continuous potential with a common integrable lower envelope gives positive finite evidence and a proper posterior.

A centered Gaussian law on a separable Banach space has an exponential-square moment.

Facts & Assumptions

Given: The hypotheses in the Statement.

[A1]

AC is assumed, as required by the centered Borel Gaussian interface and the pCN algorithm. The Axiom of Choice Prior-preserving Crank–Nicolson sampler

[F1]

The pCN proposal is $V_{β} = \sqrt{1 - β^{2}} U + β ξ$ , and its acceptance for finite potential values is $\min {1, \exp (Φ (U) - Φ (V_{β}))}$ . Prior-preserving Crank–Nicolson sampler

[F2]

A prior on a full-mass Borel forward domain and a finite continuous potential with a common integrable lower envelope have positive finite evidence and a normalized posterior. A Borel prior concentrated on a forward-map domain Misfit evidence and the potential posterior law Function-space posterior propriety from a common lower envelope

[F3]

A centered Borel Gaussian random element in a separable Banach space has $E e^{a ∥ X ∥^{2}} < \infty$ for some $a > 0$ ; a centered Borel Gaussian probability on $H$ is realized by the identity random element on $(H, B (H), μ_{0})$ . Centered Borel Gaussian random element on a separable Banach space Fernique integrability for a separable Banach Gaussian law

[F4]

If a nonnegative measurable function has integral zero, it vanishes almost everywhere; integrating on a measurable set is integrating its indicator times the function. A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere Integral over a measurable subset

[F5]

If measurable functions converge pointwise and are dominated in absolute value by one integrable function, their integrals converge to the integral of the pointwise limit. Dominated convergence

[F6]

Since $H$ is separable, countable dense $D \subseteq H$ and positive rational radii give a countable base of open norm balls in its induced metric topology: for $x \in U$ with $U$ open, choose $r > 0$ with $B (x, r) \subseteq U$ , then $d \in D$ with $∥ d - x ∥ < r / 3$ and a rational $s$ with $∥ d - x ∥ < s < r - ∥ d - x ∥$ ; then $x \in B (d, s) \subseteq B (x, r)$ . Thus $H$ is second-countable and $B (H \times H) = B (H) \otimes B (H)$ . The law notation in the Statement makes $U$ and $ξ$ Borel random elements; the pair $(U, ξ)$ is measurable into the product sigma-algebra because inverse images of measurable rectangles are intersections of measurable coordinate events. For each $β$ , $(u, z) \mapsto \sqrt{1 - β^{2}} u + β z$ is continuous, so $V_{β}$ is Borel; composing with the Borel $Φ$ and the continuous scalar operations shows $Δ_{β} = Φ (V_{β}) - Φ (U)$ and $α_{β} = \min {1, e^{- Δ_{β}}}$ are measurable. Separability: the existence of an at most countable dense subset Second countability: an at most countable basis for the topology The product sigma-algebra and its finite iterates Law or distribution of a random element Independent random elements A product of two at most countable sets is at most countable $Q$ is countably infinite The rationals embed densely in the reals A norm on a real vector space, the induced metric, and the dictionary with the metric axioms Open ball, closed ball and sphere in a metric space 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 Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed Every subset of an at most countable set is at most countable Borel sigma-algebra of a product of second-countable spaces A continuous map has Borel preimages of Borel sets Composition with a Borel measurable outer map preserves measurability Arithmetic and lattice operations preserve measurability whenever they are defined The exponential function is strictly increasing

Proof

Given: The hypotheses and definitions in the Statement.

1.1F2F4givenconstruct

Apply [F2] with parameter space $H$ , domain $D = H$ , one-point data space ${*}$ , potential $\tilde{Φ} (u, *) = Φ (u)$ , and envelope $M_{1} = 0$ . The domain has full $μ_{0}$ -mass. For any $u \in H$ , choose $R > ∥ u ∥$ ; all sufficiently close $v$ satisfy $\max {∥ u ∥, ∥ v ∥} < R$ , so the stated Lipschitz bound proves continuity at $u$ . Also $\int_{H} e^{M_{1} (∥ u ∥)} μ_{0} (d u) = 1$ . Hence $0 < Z < \infty$ and $μ$ is a probability. The density $e^{- Φ}$ is strictly positive everywhere. If $μ (A) = 0$ , then $\int_{H} e^{- Φ} 1_{A} d μ_{0} = 0$ , so [F4] gives $e^{- Φ} 1_{A} = 0$ $μ_{0}$ -almost everywhere; strict positivity yields $μ_{0} (A) = 0$ . Conversely, $μ_{0} (A) = 0$ implies $μ (A) = 0$ directly from the integral formula. Thus $μ$ and $μ_{0}$ are equivalent.

1.2F1F6givenchoosealgebra

Fix any sequence $β_{n} \in [0, 1]$ with $β_{n} \to 0$ . For every realization with $U, ξ \in H$ , $ρ_{n} : = \sqrt{1 - β_{n}^{2}} \to 1$ and $∥ V_{β_{n}} - U ∥ \leq ∣ 1 - ρ_{n} ∣ ∥ U ∥ + β_{n} ∥ ξ ∥ ⟶ 0.$ Choose $R > ∥ U ∥ + 1$ for that realization. Eventually $\max {∥ U ∥, ∥ V_{β_{n}} ∥} < R$ , and the assumed ball-wise Lipschitz bound gives $∣ Φ (V_{β_{n}}) - Φ (U) ∣ \leq L_{R} ∥ V_{β_{n}} - U ∥ ⟶ 0.$ Therefore $Δ_{n} : = Φ (V_{β_{n}}) - Φ (U) \to 0$ almost surely. Its measurability, and that of $α_{β_{n}}$ , was established in [F6].

2.1A1F3step 1.1givenalgebra

View the identity map $x \mapsto x$ on $(H, B (H), μ_{0})$ as a centered Borel Gaussian random element. By [F3], there is $a > 0$ such that $\int_{H} e^{a ∥ x ∥^{2}} μ_{0} (d x) < \infty$ . For every $q > 0$ , the function $r \mapsto r^{q} e^{- a r^{2}}$ is bounded on $[0, \infty)$ , so $\int_{H} ∥ x ∥^{q} μ_{0} (d x) < \infty$ . Since $e^{- Φ} \leq 1$ and $Z > 0$ , $E ∥ U ∥^{q} = Z^{- 1} \int_{H} ∥ x ∥^{q} e^{- Φ (x)} μ_{0} (d x) \leq Z^{- 1} \int_{H} ∥ x ∥^{q} μ_{0} (d x) < \infty .$ The same Gaussian moment bound gives $E ∥ ξ ∥^{q} < \infty$ for every $q > 0$ .

3.1F5F6step 2.1step 1.2givenalgebra

The growth bound and $∥ V_{β_{n}} ∥ \leq ∥ U ∥ + ∥ ξ ∥$ imply $∣ Δ_{n} ∣ \leq 2 K + K ∥ U ∥^{p} + K (∥ U ∥ + ∥ ξ ∥)^{p} \leq C_{p, K} (1 + ∥ U ∥^{p} + ∥ ξ ∥^{p}),$ where the last inequality follows from $(a + b)^{p} \leq 2^{p} (a^{p} + b^{p})$ for $a, b \geq 0$ (use $a + b \leq 2 \max (a, b)$ and $\max (a, b)^{p} \leq a^{p} + b^{p}$ ), with $C_{p, K} : = \max {2 K, K (1 + 2^{p}), K 2^{p}}$ . By step 2.1 the right side is integrable and does not depend on $n$ . Applying [F5] to the measurable sequence $∣ Δ_{n} ∣$ from [F6] and step 1.2 gives $E ∣ Δ_{n} ∣ \to 0$ .

4.1F5F6step 1.2givenalgebra∎

The scalar function $g (t) = \min {1, e^{- t}}$ is continuous and $g (0) = 1$ . Step 1.2 therefore implies $α_{β_{n}} = g (Δ_{n}) \to 1$ almost surely. Since $0 \leq α_{β_{n}} \leq 1$ , [F5] with the integrable dominating constant $1$ yields $E α_{β_{n}} \to 1$ . The sequence $β_{n} \to 0$ was arbitrary, so the sequential criterion for real limits proves $\lim_{β ↓ 0} E [α_{β}] = 1$ . This is the stationary mean acceptance limit; it asserts no convergence or mixing rate for the resulting chain.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

157 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

S. L. Cotter, G. O. Roberts, A. M. Stuart, and D. White, MCMC Methods for Functions: Modifying Old Algorithms to Make Them Faster, Statistical Science 28(3) (2013) (standard reference, not scraped)