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.

The wavelet product prior is L2-valued

Statement

Let $H$ be a real Hilbert space with a countable orthonormal basis $(ψ_{l k})$ , where $K_{l}$ is the level- $l$ index set and $∣ K_{l} ∣ = 2^{l}$ for each $l \geq 0$ (Hilbert space, Orthonormal families, complete orthonormal systems and Hilbert bases). Such an $H$ is separable because finite rational linear combinations of the countable basis are dense. Let $ξ_{l k}$ be IID real random variables with common density $φ$ and finite second moment $m_{2} = \int x^{2} φ (x) d x < \infty$ (Identical distribution and IID families). For $α > 0$ , set $σ_{l} = 2^{- l (α + 1 / 2)}$ and form the partial wavelet sums

$f_{N} = \sum_{0 \leq l \leq N} \sum_{k \in K_{l}} σ_{l} ξ_{l k} ψ_{l k} .$

Assume countable choice, denoted ${A C}_{ω}$ , when specializing to $H = L^{2} ([0, 1])$ . Then $f_{N}$ converges almost surely in $H$ to a Borel $H$ -valued random element $f$ , and

$E ∥ f ∥_{H}^{2} = m_{2} \sum_{l \geq 0} 2^{l} σ_{l}^{2} = m_{2} \sum_{l \geq 0} 2^{- 2 α l} < \infty .$

The abstract Hilbert-space assertion is choice-free; for $H = L^{2} ([0, 1])$ , completeness follows from the Riesz–Fischer theorem under countable choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The space $L^{p} (μ)$ as the quotient by null functions, Riesz-Fischer completeness of $L^{p}$ for $1 \leq p \leq \infty$ ). More generally, finitely many additional coarsest orthogonal coordinates with fixed scales and finite coefficient second moments may be added; they contribute only a finite expectation to the displayed sum.

Facts & Assumptions

Given: The orthonormal wavelet basis, $α > 0$ , and an IID coefficient family with density $φ$ and finite second moment $m_{2}$ ; countable choice is additionally assumed only for the $L^{2}$ specialization.

[F1]

Hilbert space: A real Hilbert space is complete in the norm induced by its inner product.

[F2]

Orthonormal families, complete orthonormal systems and Hilbert bases: Vectors in an orthonormal family are pairwise orthogonal and have norm one.

[F3]

Identical distribution and IID families: IID means mutual independence together with equality of all coordinate laws; it imposes no moment hypothesis.

[F4]

Monotone convergence for the integral: For nonnegative measurable functions increasing pointwise to $S$ , their integrals increase to $\int S$ .

[F5]

Riesz-Fischer completeness of $L^{p}$ for $1 \leq p \leq \infty$ : Under countable choice, $L^{2} ([0, 1])$ with its usual norm is complete.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): Countable choice is assumed only to apply [F5] in the $L^{2}$ instance; the abstract complete-Hilbert-space argument makes no choice-axiom appeal.

Proof

1.1F2F3F4givenalgebra

For each finite $N$ , orthonormality [F2] gives $∥ f_{N} ∥_{H}^{2} = \sum_{0 \leq l \leq N} \sum_{k \in K_{l}} σ_{l}^{2} ξ_{l k}^{2} .$ The nonnegative partial sums increase to the full coefficient-square sum, so [F4] gives its expectation as the limit of the finite expectations, $\sum_{l \geq 0} \sum_{k \in K_{l}} σ_{l}^{2} E ξ_{l k}^{2} = m_{2} \sum_{l \geq 0} 2^{l} 2^{- 2 l (α + 1 / 2)} = m_{2} \sum_{l \geq 0} 2^{- 2 α l} < \infty,$ since the final series is geometric with ratio $2^{- 2 α} < 1$ . If the coefficient-square sum were infinite on an event of probability $p > 0$ , its expectation would be at least $R p$ for every $R > 0$ , contradicting finiteness. Thus that sum is finite almost surely.

2.1A1F1F2F5givenalgebrastep 1.1

On the probability-one event where that sum is finite, for $M > N$ orthonormality gives $∥ f_{M} - f_{N} ∥_{H}^{2} = \sum_{N < l \leq M} \sum_{k \in K_{l}} σ_{l}^{2} ξ_{l k}^{2} .$ The right side tends to zero uniformly over $M > N$ as $N \to \infty$ , since it is a tail of a convergent nonnegative series. Thus $(f_{N})$ is Cauchy in $H$ and has a limit $f$ by completeness [F1]. When $H = L^{2} ([0, 1])$ , completeness is supplied by [F5] under [A1]. The Cauchy event is measurable because it is a countable combination of conditions on the measurable distances $∥ f_{M} - f_{N} ∥_{H}$ . On that event the pointwise limit is measurable as a limit into the separable metric space $H$ ; setting the limit equal to zero on the measurable complement gives a Borel $H$ -valued random element.

3.1F3F4step 2.1∎

The same monotone-convergence calculation in [F4] gives $E ∥ f ∥_{H}^{2} = E \sum_{l \geq 0} \sum_{k \in K_{l}} σ_{l}^{2} ξ_{l k}^{2} = m_{2} \sum_{l \geq 0} 2^{- 2 α l} < \infty .$ This proves both the stated second-moment formula and the claimed well-definedness.

Depends on

Used by

Dependency tree · two levels

43 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 proof of 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 proof of Theorem 7.3.12, printed pp. 583–585 (standard reference, not scraped)