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.

Nonlinear-functional BvM limit under fast L2 contraction

Statement

Use the white-noise experiment, product prior, and supplied posterior kernel of Weak nonparametric Bernstein–von Mises theorem for product priors, with all its stated basis, coefficient-density, truth, and countable-choice hypotheses. Let $Ψ : L^{2} ([0, 1]) \to R$ be Borel measurable. Suppose $f_{0} \in L^{2}$ , and for some $g \in H_{2}^{s}$ , $s > 1 / 2$ , $g \neq 0$ , $C < \infty$ , and $ρ > 0$ , $∣ Ψ (f_{0} + h) - Ψ (f_{0}) - ⟨ h, g ⟩_{L^{2}} ∣ \leq C ∥ h ∥_{2}^{2} whenever ∥ h ∥_{2} \leq ρ .$ Assume the posterior contracts in $L^{2}$ at a deterministic radius $r_{n} = o (n^{- 1 / 2})$ , meaning $Π_{n} (∥ f - f_{0} ∥_{2} > r_{n} ∣ X^{(n)}) = o_{P_{f_{0}}^{(n)}} (1)$ . Define the efficient center $θ_{n}^{*} : = Ψ (f_{0}) + L_{g} (X^{(n)} - f_{0}),$ where the last pairing is the continuous $H (δ)$ extension from Smooth functionals extend continuously to the white-noise topology. Then the posterior law of $\sqrt{n} {Ψ (f) - θ_{n}^{*}}$ converges in bounded-Lipschitz distance to $N (0, ∥ g ∥_{2}^{2})$ in $P_{f_{0}}^{(n)}$ -probability. The equal-tailed posterior interval for $Ψ (f)$ at level $1 - α$ is credible and has frequentist coverage tending to $1 - α$ .

The stipulated radius implies the source's squared-radius condition: with $s_{n} = r_{n}^{2}$ , one has $s_{n} = o (n^{- 1 / 2})$ and posterior mass inside $∥ f - f_{0} ∥_{2}^{2} \leq s_{n}$ tends to one. However, for $g \neq 0$ this radius is incompatible with the imported weak BvM limit. Thus the implication under the retained radius is vacuous; the source's squared-radius condition does not have this incompatibility.

Facts & Assumptions

Given: The product-prior weak BvM model of [F1], the Borel functional $Ψ$ , the stated local quadratic expansion with nonzero Riesz representer $g$ , the posterior $L^{2}$ radius $r_{n} = o (n^{- 1 / 2})$ , and $0 < α < 1$ .

[F1]

Weak nonparametric Bernstein–von Mises theorem for product priors: the posterior law of $\sqrt{n} (f - X^{(n)})$ converges in bounded-Lipschitz distance on $H (δ)$ to the canonical white-noise law for every $δ > 1 / 2$ .

[F2]

Smooth functionals extend continuously to the white-noise topology: $L_{g}$ extends continuously from $L^{2}$ to $H (δ)$ .

[F3]

White noise is a Borel Gaussian law on the negative Sobolev space: $L_{g} (W)$ is exactly $N (0, ∥ g ∥_{2}^{2})$ under the true white-noise law.

[F4]

Posterior quantiles stabilize under scalar weak convergence: scalar bounded-Lipschitz convergence to a CDF continuous on $R$ and locally strictly increasing at the target quantile implies quantile convergence.

[F5]

Equal-tailed posterior quantile intervals are credible: equal-tailed posterior quantiles define a measurable credible interval of 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 supplies the $L^{2}$ prior construction in [F1] and the density normal-law interface [F6]; no full choice is used below.

Proof

1.1givenalgebra

On the posterior event $∥ f - f_{0} ∥_{2} \leq r_{n} \leq ρ$ , write $R (f) = Ψ (f) - Ψ (f_{0}) - L_{g} (f - f_{0})$ . The expansion gives $\sqrt{n} ∣ R (f) ∣ \leq C \sqrt{n} r_{n}^{2} \to 0$ . Outside the event, posterior mass is $o_{P_{f_{0}}^{(n)}} (1)$ by assumption. Hence for every $ε > 0$ , $Π_{n} (\sqrt{n} ∣ R (f) ∣ > ε ∣ X^{(n)}) \to 0$ in $P_{f_{0}}^{(n)}$ -probability.

2.1A1F1F2F3step 1.1algebra

For posterior draws, $\sqrt{n} {Ψ (f) - θ_{n}^{*}} = \sqrt{n} L_{g} (f - X^{(n)}) + \sqrt{n} R (f)$ . For $c_{g} = \max (1, ∥ L_{g} ∥)$ , composing a bounded $1$ -Lipschitz scalar test with $L_{g}$ and dividing by $c_{g}$ gives an admissible bounded-Lipschitz test on $H (δ)$ . Thus the first term has bounded-Lipschitz distance to the pushforward limit at most $c_{g}$ times the distance in [F1]; by [F3] that limit is $N (0, ∥ g ∥_{2}^{2})$ . For any bounded $1$ -Lipschitz test function, replacing the first term by its sum with the remainder changes its posterior integral by at most $ε + 2 Π_{n} (\sqrt{n} ∣ R (f) ∣ > ε ∣ X^{(n)})$ . Step 1.1 and then $ε ↓ 0$ prove the asserted scalar BvM limit.

3.1F4F5F6step 2.1algebra

Apply [F4] to the centered and scaled posterior law in step 2.1. By [F6], its $α / 2$ and $1 - α / 2$ quantiles converge in probability to $∥ g ∥_{2} z_{α / 2}$ and $∥ g ∥_{2} z_{1 - α / 2}$ . Translating and rescaling these quantiles gives the equal-tailed posterior interval for $Ψ (f)$ ; its credibility follows from [F5].

4.1F3F6step 3.1algebra

Under the true experiment, $\sqrt{n} {θ_{n}^{*} - Ψ (f_{0})} = L_{g} (W)$ has exactly the law $N (0, ∥ g ∥_{2}^{2})$ by [F3]. The random centered interval endpoints in step 3.1 converge in probability to the corresponding normal quantiles. For any fixed $ε > 0$ , on the event that both endpoints are within $ε$ of their limits, coverage is bounded by deterministic normal-interval probabilities with endpoints enlarged or contracted by $ε$ . This argument requires no independence between the endpoints and $L_{g} (W)$ . By [F6], the mass of shrinking endpoint neighborhoods vanishes; letting $n \to \infty$ and then $ε ↓ 0$ gives coverage $1 - α$ .

5.1F1F2F3F6step 2.1givenconstructalgebra∎

To verify the caveat, put $Q = N (0, ∥ g ∥_{2}^{2})$ , whose density is bounded by $M = (2 π ∥ g ∥_{2}^{2})^{- 1 / 2}$ by [F6]. Choose $0 < a \leq 1$ with $2 a M < 1 / 2$ and set $c_{n} = - \sqrt{n} L_{g} (X^{(n)} - f_{0})$ . For each realized data set, $h_{n} (x) = (a - ∣ x - c_{n} ∣)_{+}$ is a bounded $1$ -Lipschitz test. On $∥ f - f_{0} ∥_{2} \leq r_{n}$ , its value at $\sqrt{n} L_{g} (f - X^{(n)})$ is at least $a - \sqrt{n} ∥ g ∥_{2} r_{n}$ , so its posterior integral tends to $a$ in probability. But $\int h_{n} d Q \leq 2 a^{2} M < a / 2$ for every center $c_{n}$ . The bounded-Lipschitz distance is a supremum over all such tests for each data set, so it cannot tend to zero. This contradicts the linear pushforward of [F1] established in step 2.1 and proves the incompatibility.

Depends on

Used by

A quadratic remainder at L2 radius n^(-1/4) 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 4 and §2.3.2 (standard reference, not scraped)
Giné and Nickl, Mathematical Foundations of Infinite-Dimensional Statistical Models, §§7.3.4–7.3.5 (standard reference, not scraped)