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

Linear-functional BvM limit and credible-interval calibration

Statement

Use the product-prior white-noise model and supplied posterior kernel of Weak nonparametric Bernstein–von Mises theorem for product priors, including its wavelet-basis, coefficient-density, truth, and countable-choice hypotheses. Let $g \in H_{2}^{s}$ for some $s > 1 / 2$ , with $g \neq 0$ , and put $σ_{g} = ∥ g ∥_{2}$ . Let $Q_{n}$ be the posterior law of $L_{g} (f)$ and let $C_{n, α} = [q_{α / 2} (Q_{n}), q_{1 - α / 2} (Q_{n})], 0 < α < 1.$ Then $β_{B L, R} ⁣ (Q_{n} \circ [u \mapsto \sqrt{n} (u - L_{g} (X^{(n)}))]^{- 1}, N (0, σ_{g}^{2})) ⟶ 0$ in $P_{f_{0}}^{(n)}$ -probability. The interval $C_{n, α}$ is posterior credible at level $1 - α$ , and its frequentist coverage satisfies $P_{f_{0}}^{(n)} {L_{g} (f_{0}) \in C_{n, α}} ⟶ 1 - α .$

Facts & Assumptions

Given: The white-noise experiment, product prior, posterior kernel, basis, density and truth assumptions of Weak nonparametric Bernstein–von Mises theorem for product priors, together with $g \neq 0$ , $g \in H_{2}^{s}$ , $s > 1 / 2$ , and $0 < α < 1$ .

[F1]

Weak nonparametric Bernstein–von Mises theorem for product priors: for every $δ > 1 / 2$ , the posterior law of $\sqrt{n} (f - X^{(n)})$ converges in bounded-Lipschitz distance in $H (δ)$ to the canonical white-noise law $N$ in $P_{f_{0}}^{(n)}$ -probability. Its product-prior construction requires countable choice; the same axiom suffices for the scalar density-normal interface.

[F2]

Smooth functionals extend continuously to the white-noise topology: $L_{g}$ is a continuous linear functional on $H (δ)$ and agrees with $f \mapsto ⟨ f, g ⟩_{L^{2}}$ on $L^{2}$ .

[F3]

White noise is a Borel Gaussian law on the negative Sobolev space: the canonical law $N$ is centered Gaussian on $H (δ)$ ; for the coefficient pairing $L_{g}$ , its variance is $\sum_{l, k} ∣ g_{l k} ∣^{2} = ∥ g ∥_{2}^{2}$ .

[F4]

Posterior quantiles stabilize under scalar weak convergence: bounded-Lipschitz convergence in probability to a law with continuous CDF locally strictly increasing at an interior quantile implies convergence in probability of that posterior quantile.

[F5]

Equal-tailed posterior quantile intervals are credible: the equal-tailed interval between posterior quantiles $q_{α / 2}$ and $q_{1 - α / 2}$ is graph-measurable and has posterior mass at least $1 - α$ .

[F6]

Density normal laws and square-summable Gaussian series under countable choice: Under countable choice, in its density convention, $N (0, 1)$ is defined by its continuous positive density, and $N (0, σ^{2})$ for $σ > 0$ is its image under $x \mapsto σ x$ ; change of variables gives a continuous strictly positive density and hence a continuous strictly increasing CDF.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): countable choice is inherited through [F1] for the $L^{2}$ product-prior construction and also suffices for the density normal-law interface [F6]; no full choice is used below.

Proof

1.1A1F1F2F3algebra

Fix $δ > 1 / 2$ . For every bounded $1$ -Lipschitz function $h : R \to R$ , the composition $h \circ L_{g}$ is bounded by $1$ and has Lipschitz constant at most $∥ L_{g} ∥_{H (δ)^{*}}$ . Rescaling by $c_{g} = \max (1, ∥ L_{g} ∥_{H (δ)^{*}})$ makes it an admissible bounded-Lipschitz test on $H (δ)$ . Hence the scalar pushforward distance is at most $c_{g}$ times the distance in [F1]. The pushforward of $N$ is $N (0, σ_{g}^{2})$ by [F3], proving the asserted scalar BvM limit.

2.1F4F5F6step 1.1algebra

Translate the posterior law of $L_{g} (f)$ by $L_{g} (X^{(n)})$ and scale by $\sqrt{n}$ . By [F4] and the continuous strictly increasing normal CDF from [F6], the two quantiles of this scaled law converge in probability to $σ_{g} z_{α / 2}$ and $σ_{g} z_{1 - α / 2}$ , where $z_{u}$ is the $u$ -quantile of $N (0, 1)$ . Since the affine map is increasing, these are exactly the scaled endpoints of $C_{n, α} - L_{g} (X^{(n)})$ . The interval is credible by [F5].

3.1F3F6step 2.1algebra

Under the true white-noise law, $\sqrt{n} {L_{g} (X^{(n)}) - L_{g} (f_{0})} = L_{g} (W)$ has exactly the centered normal law $N (0, σ_{g}^{2})$ by [F3]. On the event that both random scaled endpoints in step 2.1 lie within $ε$ of their limits, the event $L_{g} (f_{0}) \in C_{n, α}$ is bounded between the corresponding deterministic normal-interval events with endpoints enlarged or contracted by $ε$ . This sandwich uses no independence between the endpoints and the observation. The endpoint event has probability tending to one, and [F6] makes the normal mass of shrinking neighborhoods of the two endpoints tend to zero.

4.1F6step 3.1algebra∎

Letting $n \to \infty$ and then $ε ↓ 0$ in the sandwich of step 3.1 gives limiting coverage $Φ (z_{1 - α / 2}) - Φ (z_{α / 2}) = 1 - α$ by the definition of the normal quantiles and CDF in [F6].

Depends on

Used by

The integral functional under a product-prior white-noise BvM Example

Dependency tree · two levels

42 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

Castillo and Nickl, Nonparametric Bernstein–von Mises theorems in Gaussian white noise, Theorem 3 and §2.3.1 (standard reference, not scraped)
Giné and Nickl, Mathematical Foundations of Infinite-Dimensional Statistical Models, §§7.3.4–7.3.5 (standard reference, not scraped)