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

Projected empirical bridge CLT in the little-o multiscale space

Statement

Assume AC. Let $P_{0}$ have a density $f_{0}$ on $[0, 1]$ with $∥ f_{0} ∥_{\infty} \leq B < \infty$ . Let $(ψ_{l k})$ be an orthonormal, compactly supported wavelet basis with $2^{l}$ coefficients at level $l \geq 1$ , uniformly bounded overlap, and $∥ ψ_{l k} ∥_{\infty} \leq C_{0} 2^{l / 2}$ . Suppose for some $γ > 1 / 2$ , $\max_{k} ∣ ⟨ f_{0}, ψ_{l k} ⟩ ∣ \leq C_{f} 2^{- l (γ + 1 / 2)} .$ Let $w_{l} \geq 1$ be nondecreasing and admissible in Little-o multiscale coefficient space M0(w), and choose either cutoff regime $2^{L_{n}} ≍ n^{1 / (2 γ + 1)} or 2^{L_{n}} ≍ (n / \log n)^{1 / (2 γ + 1)} .$ For IID $X_{1}, \dots, X_{n} \sim P_{0}$ , define the finite wavelet projection $P_{n} (L_{n})$ by coefficients $⟨ P_{n} (L_{n}), ψ_{l k} ⟩ = P_{n} ψ_{l k} : = n^{- 1} \sum_{i = 1}^{n} ψ_{l k} (X_{i})$ for $l \leq L_{n}$ and zero for $l > L_{n}$ , with the coarsest scaling coordinates projected as well. Let $G_{P_{0}}$ be a Borel centered Gaussian law on $M_{0} (w)$ whose coefficient covariance is $Cov (G_{l k}, G_{l^{'} k^{'}}) = P_{0} [(ψ_{l k} - P_{0} ψ_{l k}) (ψ_{l^{'} k^{'}} - P_{0} ψ_{l^{'} k^{'}})] .$ Then $\sqrt{n} {P_{n} (L_{n}) - f_{0}} \Rightarrow G_{P_{0}} in M_{0} (w) .$

Facts & Assumptions

Given: AC, the density and wavelet bounds, the coefficient smoothness and cutoff conditions, IID observations, and the stated Borel Gaussian bridge law.

[F1]

Little-o multiscale coefficient space M0(w): $M_{0} (w)$ uses the norm $\sup_{l} w_{l}^{- 1} \max_{k} ∣ x_{l k} ∣$ , with normalized level maxima tending to zero.

[F2]

The multiscale coefficient space is separable and has vanishing projection tails: square-summable coefficient sequences lie in $M_{0} (w)$ , and finite-level projections converge in its norm.

[F3]

Finite-projection convergence and posterior tail control imply weak BvM: convergence of every fixed finite projection together with vanishing tails under the approximating and limit laws implies bounded-Lipschitz convergence on $M_{0} (w)$ .

[F4]

Multivariate iid central limit theorem: under AC, finite-second-moment IID vectors have the multivariate normal limit with their covariance, including singular covariance.

[F5]

The bounded-Lipschitz metric characterizes weak convergence on Polish spaces: on finite-dimensional Euclidean space, weak convergence of Borel probabilities implies convergence in bounded-Lipschitz distance.

[F6]

Finite and countable subadditivity of measures: a probability of a finite union is bounded by the sum of the component probabilities.

[F7]

Markov's inequality for random variables: for nonnegative $Y$ and $a > 0$ , $\Pr (Y \geq a) \leq E [Y] / a$ .

[F8]

Continuity from above when one set has finite measure: probabilities of decreasing measurable sets with finite first measure converge to the probability of their intersection.

[F9]

Identical distribution and IID families: IID means the observations are mutually independent and have a common law.

[A1]

The Axiom of Choice: AC is the stated axiom used by [F4] for finite-dimensional CLTs; no common null set over all directions is required because each projection level $J$ is fixed.

[A2]

The basis satisfies the uniform support, overlap, coefficient-count and sup-norm bounds in the Statement.

[A3]

The truth coefficients satisfy the displayed $C_{f} 2^{- l (γ + 1 / 2)}$ bound.

Proof

Given: The probability law, basis, coefficient smoothness, admissible weights, cutoff, Gaussian limit law, and AC hypothesis in the Statement.

1.1F2givenalgebra

$P_{n} (L_{n})$ has finitely many nonzero coefficients, so it is in $M_{0} (w)$ . The coefficient sequence of $f_{0}$ is square-summable by Parseval, so [F2] places it in $M_{0} (w)$ . Thus $U_{n} = \sqrt{n} {P_{n} (L_{n}) - f_{0}}$ is a well-defined $M_{0} (w)$ -valued random element.

1.2A1A2F4F5F9given

Fix $J$ . For all sufficiently large $n$ , $L_{n} \geq J$ , so the coordinates of $P_{J} U_{n}$ are $n^{- 1 / 2} \sum_{i = 1}^{n} (ψ_{l k} (X_{i}) - P_{0} ψ_{l k})$ for the finitely many indices through level $J$ . The vector summand is bounded by [A2], has finite second moment, and is IID by [F9]; its covariance is the displayed covariance of $G_{P_{0}}$ . By [F4] these finite-dimensional vectors converge weakly to the corresponding Gaussian projection. The projection space is finite-dimensional Euclidean with an equivalent weighted maximum norm, so [F5] gives convergence in bounded-Lipschitz distance for every fixed $J$ .

1.3A2F7givenalgebra

Let $Y_{i} = ψ_{l k} (X_{i}) - P_{0} ψ_{l k}$ . Then $E Y_{i} = 0$ , $E Y_{i}^{2} \leq P_{0} ψ_{l k}^{2} \leq B$ , and $∣ Y_{i} ∣ \leq 2 C_{0} 2^{l / 2} = : b_{l}$ by [A2]. For $m \geq 2$ , $E ∣ Y_{i} ∣^{m} \leq b_{l}^{m - 2} E Y_{i}^{2}$ . Since $m! \geq 2 3^{m - 2}$ , expansion of the exponential gives, for $0 < λ b_{l} < 3 \sqrt{n}$ , $E \exp (λ n^{- 1 / 2} \sum_{i = 1}^{n} Y_{i}) \leq \exp (λ^{2} B / [2 (1 - λ b_{l} / (3 \sqrt{n}))])$ . Applying [F7] to this exponential and optimizing at $λ = t / (B + b_{l} t / (3 \sqrt{n}))$ yields $P_{0}^{n} {∣ \sqrt{n} (P_{n} - P_{0}) ψ_{l k} ∣ > t} \leq 2 \exp (- t^{2} / [2 (B + b_{l} t / (3 \sqrt{n}))])$ . Applying the same argument to $- Y_{i}$ supplies the lower-tail bound.

1.4A3F1givenalgebra

Above the cutoff, $U_{n}$ has only the deterministic bias coefficients $- \sqrt{n} ⟨ f_{0}, ψ_{l k} ⟩$ . By [A3] and monotonicity of $w_{l}$ , $\sup_{l > L_{n}, k} \sqrt{n} ∣ ⟨ f_{0}, ψ_{l k} ⟩ ∣ / w_{l} \leq C_{f} \sqrt{n} 2^{- L_{n} (γ + 1 / 2)} / w_{L_{n}}$ . For the first cutoff regime the numerator is bounded, while $w_{L_{n}} \to \infty$ . For the second, the numerator is $O (\sqrt{\log n})$ and $\sqrt{L_{n}} ≍ \sqrt{\log n}$ ; admissibility $w_{L_{n}} / \sqrt{L_{n}} \to \infty$ again makes the ratio vanish.

2.1F1F6step 1.3givenalgebra

Fix $ε > 0$ . By [F6] and step 1.3, $P_{0}^{n} {\max_{J < l \leq L_{n}, k} ∣ \sqrt{n} (P_{n} - P_{0}) ψ_{l k} ∣ / w_{l} > ε} \leq \sum_{J < l \leq L_{n}} 2^{l + 1} \exp (- ε^{2} w_{l}^{2} / [2 (B + (2 C_{0} ε / 3) 2^{l / 2} w_{l} / \sqrt{n})])$ . For levels with $2^{l / 2} w_{l} / \sqrt{n} \leq 1$ , the denominator is bounded by a constant depending only on $B, C_{0}, ε$ . Their sum is bounded by $\sum_{l > J} 2^{l + 1} e^{- c_{ε} w_{l}^{2}}$ , which tends to zero as $J \to \infty$ : admissibility gives $w_{l}^{2} / l \to \infty$ , so the summand is eventually bounded by $2^{- l}$ .

3.1step 2.1givenalgebra

For the remaining levels $2^{l / 2} w_{l} / \sqrt{n} > 1$ , the exponent in step 2.1 is at least $c_{ε} w_{l} \sqrt{n} / 2^{l / 2} \geq c_{ε} \sqrt{n} / 2^{L_{n} / 2}$ . Their total contribution is at most $2^{L_{n} + 2} \exp (- c_{ε} \sqrt{n} / 2^{L_{n} / 2})$ , which tends to zero. Indeed $L_{n} = O (\log n)$ and either cutoff gives $\sqrt{n} / 2^{L_{n} / 2} \geq c n^{γ / (2 γ + 1)}$ for all large $n$ after decreasing $c > 0$ if needed; this polynomial growth dominates $L_{n} \log 2$ .

4.1step 2.1step 3.1algebra

The two threshold classes partition all levels $J < l \leq L_{n}$ . The low-threshold sum tends to zero as $J \to \infty$ by step 2.1, and the high-threshold sum tends to zero as $n \to \infty$ by step 3.1. Therefore the centered empirical-fluctuation tails vanish in the iterated limit $n \to \infty$ , then $J \to \infty$ .

5.1F2F8step 4.1step 1.4

For the fixed Gaussian law $G_{P_{0}}$ , [F2] gives $∥ G_{P_{0}} - P_{J} G_{P_{0}} ∥_{M (w)} \to 0$ pointwise. Hence the events ${∥ G_{P_{0}} - P_{J} G_{P_{0}} ∥_{M (w)} > ε}$ decrease to the empty set; [F8] makes their probabilities tend to zero. Steps 4.1 and 1.4 give the matching posterior-tail condition for the laws of $U_{n}$ .

6.1F3step 1.2step 4.1step 1.4step 5.1∎

For each fixed $J$ , step 1.2 gives convergence of the projected laws in bounded-Lipschitz distance; steps 4.1 and 1.4 give vanishing tails for $U_{n}$ , and step 5.1 gives vanishing tails for $G_{P_{0}}$ . Applying [F3] to these laws proves $β_{B L} (L (U_{n}), G_{P_{0}}) \to 0$ , which is the asserted weak convergence on $M_{0} (w)$ .

Depends on

Used by

Dependency tree · two levels

38 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, On the Bernstein–von Mises phenomenon for nonparametric Bayes procedures, Theorem 1, equations (15)–(17), and §5.1 (standard reference, not scraped)
Giné and Nickl, Mathematical Foundations of Infinite-Dimensional Statistical Models, §§3.7 and 7.4 (standard reference, not scraped)