LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

A negative-Sobolev posterior second-moment bound

Statement

Use the wavelet product-prior white-noise model of The wavelet product prior is L2-valued and The product-prior posterior factors by coordinates, with $σ_{l} = 2^{- l (α + 1 / 2)}$ , $α > 0$ , and $2^{l}$ coefficients at level $l \geq 0$ . Let $θ_{0, l k}$ be the coefficients of a fixed $f_{0} \in L^{2} ([0, 1])$ . Assume countable choice for the $L^{2}$ prior construction, with the full posterior kernel supplied by The product-prior posterior factors by coordinates, and suppose

$\sup_{l, k} ∣ \frac{θ_{0, l k}}{σ_{l}} ∣ \leq M < τ,$

where the common prior density $φ$ satisfies $φ (u) \leq C_{φ}$ for all $u$ , $φ (u) \geq c_{φ} > 0$ for $∣ u ∣ < τ$ , and $m_{2} : = \int u^{2} φ (u) d u < \infty$ . For every $δ > 1 / 2$ there is a constant $C_{δ} < \infty$ , independent of $n$ , such that

$E_{f_{0}}^{(n)} \int ∥ f - f_{0} ∥_{H (δ)}^{2} Π_{n} (d f ∣ X^{(n)}) \leq \frac{C_{δ}}{n} .$

No continuity assumption on $φ$ is needed for this moment estimate.

Facts & Assumptions

[F1]

Logarithmic negative Sobolev spaces for white noise: $∥ u ∥_{H (δ)}^{2} = \sum_{l, k} w_{l}^{δ} ∣ u_{l k} ∣^{2}$ , where $w_{l}^{δ} = a_{l}^{- 1} (\log a_{l})^{- 2 δ}$ and $\sum_{l, k} w_{l}^{δ} < \infty$ for $δ > 1 / 2$ .

[F2]

The product-prior posterior factors by coordinates: Given the data coordinate $X_{l k}$ , the posterior density of $θ_{l k}$ is proportional to $e^{- n (θ - X_{l k})^{2} / 2} σ_{l}^{- 1} φ (θ / σ_{l})$ ; finite coordinate marginals factor.

[F3]

Monotone convergence for the integral: Expectations of nonnegative partial sums increasing pointwise to a limit increase to the expectation of that limit.

[F4]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: For the nonnegative Gaussian-integral integrand, expectation and Lebesgue integration may be interchanged on the sigma-finite product of the normal probability space and $R$ .

[A1]

The true normalized coordinates $r_{l k} = θ_{0, l k} / σ_{l}$ satisfy $∣ r_{l k} ∣ \leq M < τ$ , and $φ$ has the boundedness, local positivity, and second-moment properties in the statement.

[A2]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): Countable choice is used for the $L^{2}$ prior construction. The full posterior kernel is supplied as model input in [F2]; the coordinate moment estimates below require no further choice.

Given: Countable choice, the white-noise observations $X_{l k} = θ_{0, l k} + n^{- 1 / 2} Z_{l k}$ with independent standard normal coordinates, the prior, and its coordinate posterior law. The expected posterior loss bound in the Statement is to be proved.

Proof

1.1A1A2F2givenalgebra

Fix $(l, k)$ and abbreviate $σ = σ_{l}$ , $θ_{0} = θ_{0, l k}$ , $r = θ_{0} / σ$ , and $λ = \sqrt{n} σ$ . Under the true law write $X = θ_{0} + n^{- 1 / 2} Z$ , where $Z$ has density $(2 π)^{- 1 / 2} e^{- z^{2} / 2}$ . If $B_{l k} (X) = \int (θ - θ_{0})^{2} Π_{n} (d θ_{l k} ∣ X)$ , change variables $v = \sqrt{n} (θ - θ_{0})$ in [F2] to obtain $n B_{l k} (X) = \frac{N_{λ} (Z)}{D_{λ} (Z)}, D_{λ} (z) = \frac{1}{λ} \int_{R} e^{- v^{2} / 2 + z v} φ (r + v / λ) d v, N_{λ} (z) = \frac{1}{λ} \int_{R} v^{2} e^{- v^{2} / 2 + z v} φ (r + v / λ) d v .$ All integrands are nonnegative and the denominator is positive. The posterior kernel is the $L^{2}$ model supplied by [F2] under [A2].

2.1A1givenstep 1.1F4algebra

Set $h = (τ - M) / 2 > 0$ . If $λ \leq S_{0}$ for a fixed $S_{0} > 0$ , then $∣ r + v / λ ∣ < τ$ whenever $∣ v ∣ \leq h λ$ . Substituting $v = λ t$ and pairing $t$ with $- t$ gives $D_{λ} (z) \geq c_{φ} \int_{- h}^{h} e^{- λ^{2} t^{2} / 2 + z λ t} d t = 2 c_{φ} \int_{0}^{h} e^{- λ^{2} t^{2} / 2} \cosh (z λ t) d t \geq 2 h c_{φ} e^{- h^{2} λ^{2} / 2} \geq d_{0} : = 2 h c_{φ} e^{- h^{2} S_{0}^{2} / 2} > 0,$ because $\cosh (x) \geq 1$ and $e^{- λ^{2} t^{2} / 2} \geq e^{- h^{2} λ^{2} / 2}$ on $[0, h]$ . Completing the square in the standard normal density gives $E e^{Z v} = e^{v^{2} / 2}$ ; hence, by the substitution $u = r + v / λ$ , $E N_{λ} (Z) = \frac{1}{λ} \int v^{2} φ (r + v / λ) d v = λ^{2} \int (u - r)^{2} φ (u) d u \leq 2 λ^{2} (m_{2} + M^{2}) .$ Here [F4] justifies the exchange of expectation and the nonnegative $v$ -integral. Therefore $E B_{l k} (X) \leq C λ^{2} / n = C σ_{l}^{2} \leq C S_{0}^{2} / n$ in this range.

2.2A1givenstep 1.1algebra

If $λ \geq S_{0}$ , let $R = h S_{0}$ . For $∣ v ∣ \leq R$ one has $∣ r + v / λ ∣ < τ$ , so $D_{λ} (z) \geq \frac{c_{φ} e^{z^{2} / 2}}{λ} I_{R} (z), N_{λ} (z) \leq \frac{C_{φ} e^{z^{2} / 2}}{λ} J (z),$ where $I_{R} (z) = \int_{- R}^{R} e^{- (v - z)^{2} / 2} d v$ and $J (z) = \int_{R} v^{2} e^{- (v - z)^{2} / 2} d v = \sqrt{2 π} (1 + z^{2})$ . Thus $n B_{l k} (X) \leq (C_{φ} / c_{φ}) J (Z) / I_{R} (Z)$ . For $∣ z ∣ \leq R$ , integrate $I_{R}$ over the half-interval nearest $z$ ; for $∣ z ∣ > R$ , integrate over the half-interval adjacent to the nearer endpoint. These choices give the common lower bound $I_{R} (z) \geq \frac{R}{2} \exp (- \frac{R^{2}}{2} - \frac{(∣ z ∣ - R / 2)_{+}^{2}}{2}) .$ Consequently $E [J (Z) / I_{R} (Z)]$ is finite: after multiplying by the standard normal density, its integrand is bounded on $∣ z ∣ \leq R / 2$ and is at most a constant times $(1 + z^{2}) e^{- R ∣ z ∣ / 2}$ on $∣ z ∣ > R / 2$ . Hence $E B_{l k} (X) \leq C / n$ also when $λ \geq S_{0}$ , with $C$ independent of $(l, k, n)$ .

3.1step 2.1step 2.2

The two ranges in steps 2.1 and 2.2 cover every $λ > 0$ ; since $σ_{l}^{2} \leq S_{0}^{2} / n$ in the first range, there is a single constant $C$ for which $\sup_{l, k} E_{f_{0}}^{(n)} B_{l k} (X) \leq C / n$ .

4.1A1F1F3step 3.1∎

By [F1], the posterior squared loss is the nonnegative series $\sum_{l, k} w_{l}^{δ} B_{l k} (X)$ . Apply monotone convergence [F3] to its finite partial sums and use step 3.1 to obtain $E_{f_{0}}^{(n)} \int ∥ f - f_{0} ∥_{H (δ)}^{2} Π_{n} (d f ∣ X) = \sum_{l, k} w_{l}^{δ} E_{f_{0}}^{(n)} B_{l k} (X) \leq \frac{C}{n} \sum_{l, k} w_{l}^{δ} .$ The trace on the right is finite for $δ > 1 / 2$ by [F1], proving the bound.

Depends on

Used by

Weak nonparametric Bernstein–von Mises theorem for product priors Theorem

Dependency tree · two levels

34 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 5 and proof, printed pp. 2013–2016 (standard reference, not scraped)
Giné and Nickl, Mathematical Foundations of Infinite-Dimensional Statistical Models, Theorem 7.3.12 and proof, printed pp. 584–586 (standard reference, not scraped)