LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge 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.

Prior-predictive and fixed-truth data laws are equivalent

Statement

Assume countable choice. Use the wavelet product prior and white-noise model from The wavelet product prior is L2-valued and White noise is a Borel Gaussian law on the negative Sobolev space, with $α > 0$ , $σ_{l} = 2^{- l (α + 1 / 2)}$ , and a common coefficient density $φ$ having finite second moment $m_{2}$ . Let $f_{0} \in L^{2} ([0, 1])$ . For each $n \geq 1$ and $δ > 1 / 2$ , let $Q_{n}$ be the prior-predictive law on $H (δ)$ of $X = f + n^{- 1 / 2} W$ , with prior draw $f$ independent of canonical white noise $W$ , and let $P_{f_{0}}^{(n)}$ be the law of $f_{0} + n^{- 1 / 2} W$ . Then $Q_{n}$ and $P_{f_{0}}^{(n)}$ are mutually absolutely continuous as Borel probabilities on $H (δ)$ .

Facts & Assumptions

Given: The product-prior and white-noise laws, independence between the prior draw and observation noise, $α > 0$ , finite coefficient second moment $m_{2}$ , and $f_{0} \in L^{2} ([0, 1])$ .

[F1]

Logarithmic negative Sobolev spaces for white noise: $H (δ)$ is the weighted coefficient Hilbert space, its finite-coordinate projections converge in norm, and $L^{2} ([0, 1])$ embeds continuously into it.

[F2]

The wavelet product prior is L2-valued: The prior coefficients are independent with common density $φ$ , and the prior law is supported on $L^{2}$ under its stated scale and moment conditions.

[F3]

White noise is a Borel Gaussian law on the negative Sobolev space: The noise law is a Borel probability on $H (δ)$ with independent standard normal coordinates.

[F4]

The Bessel inequality for an arbitrary orthonormal family: The squared coefficient sum of $f_{0}$ is at most $∥ f_{0} ∥_{2}^{2}$ .

[F5]

Independent random elements have product joint law: A finite independent family of random elements has the product of its marginal laws as its joint law.

[F6]

Finite measures agreeing on a generating pi-system and on the whole space are equal: Finite measures agreeing on a generating pi-system and on the whole space agree on the generated sigma-algebra.

[F7]

The indefinite integral of a nonnegative measurable function is a measure: For a nonnegative measurable density $L$ , the set function $A \mapsto \int_{A} L d Q_{n}$ is a measure.

[F8]

Riesz-Fischer completeness of $L^{p}$ for $1 \leq p \leq \infty$ : Under countable choice, $L^{2} (Q_{n})$ is complete for the probability measure $Q_{n}$ .

[F9]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: Nonnegative integrands may be integrated in either order under the product of the prior coordinate law and Lebesgue measure.

[F10]

The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ : The Gaussian integral normalizes the displayed one-dimensional normal densities.

Given: All probabilities in the statement are defined on the specified Borel space; only their equivalence is proved below.

Proof

1.1F1givenalgebra

Enumerate the wavelet coefficients as $j = 1, 2, \dots$ and let $P_{m}$ retain the first $m$ coordinates. The sigma-algebra generated by all coordinate maps is the Borel sigma-algebra of $H (δ)$ . Indeed, the coordinate maps are continuous, so their sigma-algebra is contained in the Borel sigma-algebra. Conversely, for any closed set $C \subseteq H (δ)$ , $x \mapsto d (P_{m} x, C)$ is measurable with respect to the coordinate sigma-algebra and converges to $d (x, C)$ by [F1]. Thus $C = {x : d (x, C) = 0}$ belongs to that sigma-algebra.

1.2F2F3F4F5F9F10givenalgebra

Write $p_{a, n} (x) = (n / 2 π)^{1 / 2} e^{- n (x - a)^{2} / 2}$ and let $π_{j} (d t) = σ_{j}^{- 1} φ (t / σ_{j}) d t$ , where $σ_{j} = σ_{l}$ for $j = (l, k)$ . The true and prior-predictive coordinate densities are $p_{j} = p_{θ_{0, j}, n}$ and $q_{j} (x) = \int p_{t, n} (x) π_{j} (d t)$ ; both are positive probability densities by [F9, F10]. Put $h_{j}^{2} = \int (\sqrt{p_{j}} - \sqrt{q_{j}})^{2} d x$ and $ρ_{j} = \int \sqrt{p_{j} q_{j}} d x = 1 - h_{j}^{2} / 2$ . Concavity of square root and [F9] give $ρ_{j} \geq \int ⁣ [\int \sqrt{p_{θ_{0, j}, n} (x) p_{t, n} (x)} d x] π_{j} (d t)$ . Completing the square and using [F10] evaluates the inner integral as $e^{- n (t - θ_{0, j})^{2} / 8}$ . Thus $h_{j}^{2} \leq \int 2 (1 - e^{- n (t - θ_{0, j})^{2} / 8}) π_{j} (d t) \leq \frac{n}{4} \int (t - θ_{0, j})^{2} π_{j} (d t) \leq \frac{n}{2} (θ_{0, j}^{2} + σ_{j}^{2} m_{2})$ . By [F2], [F3], and [F5] the prior-predictive and true coordinates are each independent across $j$ . By [F4] and the geometric-series formula, $\sum_{j} θ_{0, j}^{2} < \infty$ and $\sum_{j} σ_{j}^{2} = \sum_{l \geq 0} 2^{- 2 α l} < \infty$ . Hence $\sum_{j} h_{j}^{2} < \infty$ and $\sum_{j} (1 - ρ_{j}) < \infty$ .

2.1F5F8step 1.2givenalgebra

Let $F_{m}$ be the sigma-algebra of the first $m$ coordinates on $H (δ)$ and set $L_{m} = \prod_{j \leq m} p_{j} (X_{j}) / q_{j} (X_{j})$ . Under $Q_{n}$ , $L_{m}$ is the density of the first $m$ true coordinates relative to the first $m$ prior-predictive coordinates, and $E_{Q_{n}} L_{m} = 1$ . By [F5], finite coordinate laws are products; hence for $r > m$ , independence gives $E_{Q_{n}} ⁣ [\sqrt{L_{r} L_{m}}] = \prod_{m < j \leq r} ρ_{j},$ so $∥ \sqrt{L_{r}} - \sqrt{L_{m}} ∥_{L^{2} (Q_{n})}^{2} = 2 (1 - \prod_{m < j \leq r} ρ_{j}) \leq 2 \sum_{m < j \leq r} (1 - ρ_{j}) \to 0$ uniformly in $r > m$ . By [F8] and countable choice, $\sqrt{L_{m}}$ has an $L^{2} (Q_{n})$ limit $G$ ; since each term is nonnegative, $∥ G^{-} ∥_{2} \leq ∥ G - \sqrt{L_{m}} ∥_{2} \to 0$ , so $G \geq 0$ almost surely. The norms $∥ \sqrt{L_{m}} ∥_{2} = 1$ give $∥ G ∥_{2} = 1$ . Put $L = G^{2}$ . Then $∥ L_{m} - L ∥_{1} \leq ∥ \sqrt{L_{m}} - G ∥_{2} ∥ \sqrt{L_{m}} + G ∥_{2} \leq 2 ∥ \sqrt{L_{m}} - G ∥_{2} \to 0$ , and $L \geq 0$ with $\int L d Q_{n} = 1$ .

3.1F5F6F7step 1.1step 2.1step 1.2∎

For every event $A \in F_{m}$ and $r \geq m$ , the finite-coordinate density identity and independence of the remaining coordinates give $\int_{A} L_{r} d Q_{n} = P_{f_{0}}^{(n)} (A)$ . Passing to the $L^{1}$ limit gives $\int_{A} L d Q_{n} = P_{f_{0}}^{(n)} (A)$ . By [F7], the nonnegative density L with total integral one defines a probability measure. Such finite-coordinate cylinder events form a generating pi-system by step 1.1; [F6] therefore gives $P_{f_{0}}^{(n)} (A) = \int_{A} L d Q_{n}$ for every Borel $A \subseteq H (δ)$ . Thus $P_{f_{0}}^{(n)} ≪ Q_{n}$ . Interchanging $p_{j}$ and $q_{j}$ gives the same argument and proves $Q_{n} ≪ P_{f_{0}}^{(n)}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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