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.

Diameter of undersmoothed multiscale credible bands

Statement

Assume all hypotheses of CDF and multiscale credible-band calibration from weak BvM limits at a fixed credibility level $1 - α$ , $0 < α < 1$ , and use its $M_{0} (w)$ credible ball $C_{n}^{M}$ and scaled radius $R_{n}^{M}$ . Let $γ > 0$ , assume the compactly supported wavelets have uniformly bounded overlap and $∥ ψ_{l k} ∥_{\infty} \leq C 2^{l / 2}$ , and define $∥ f ∥_{C_{ψ}^{γ}} : = \sup_{l, k} 2^{l (γ + 1 / 2)} ∣ ⟨ f, ψ_{l k} ⟩ ∣ .$ Suppose $∥ f_{0} ∥_{C_{ψ}^{γ}} < \infty$ . Choose integers $j_{n}$ with $2^{j_{n}} ≍ (n / \log n)^{1 / (2 γ + 1)}$ and let $u_{n} = w_{j_{n}} / \sqrt{j_{n}} \to \infty$ . Intersect the credible ball with the coefficient smoothness ball: ${\overline{C}}_{n} = C_{n}^{M} \cap {f : ∥ f ∥_{C_{ψ}^{γ}} \leq u_{n}} .$ Then $P_{f_{0}}^{(n)} {f_{0} \in {\overline{C}}_{n}} \to 1 - α$ , and its $L^{\infty}$ diameter satisfies ${diam}_{L^{\infty}} ({\overline{C}}_{n}) = O_{P_{f_{0}}^{(n)}} ⁣ ((n / \log n)^{- γ / (2 γ + 1)} u_{n}) .$

Facts & Assumptions

Given: All hypotheses, the credible ball and radius of CDF and multiscale credible-band calibration from weak BvM limits, the coefficient smoothness norm and wavelet assumptions in the Statement, $γ > 0$ , and $u_{n} \to \infty$ .

[F1]

Little-o multiscale coefficient space M0(w): the multiscale ball bounds each level- $l$ coefficient by $w_{l}$ times its radius.

[F2]

CDF and multiscale credible-band calibration from weak BvM limits: $C_{n}^{M}$ has frequentist coverage tending to $1 - α$ , and its scaled radius $R_{n}^{M}$ converges in probability to a finite quantile, hence is $O_{P} (1)$ .

[L1]

The Statement defines $C_{ψ}^{γ}$ by the displayed coefficient norm $\sup_{l, k} 2^{l (γ + 1 / 2)} ∣ ⟨ f, ψ_{l k} ⟩ ∣$ .

Proof

1.1F2L1given

Since $∥ f_{0} ∥_{C_{ψ}^{γ}} < \infty$ and $u_{n} \to \infty$ , [L1] implies the truth belongs to the coefficient smoothness ball for all sufficiently large $n$ . For those $n$ , ${f_{0} \in {\overline{C}}_{n}} = {f_{0} \in C_{n}^{M}}$ , so the asserted coverage follows from [F2].

1.2F1L1givenalgebra

Let $f, g \in {\overline{C}}_{n}$ . For $l \leq j_{n}$ , [F1] gives $\max_{k} ∣ f_{l k} - g_{l k} ∣ \leq 2 R_{n}^{M} w_{l} / \sqrt{n}$ . For $l > j_{n}$ , [L1] and membership in the coefficient smoothness ball give $\max_{k} ∣ f_{l k} - g_{l k} ∣ \leq 2 u_{n} 2^{- l (γ + 1 / 2)}$ . At each point, only a uniformly bounded number of level- $l$ wavelets are nonzero, each bounded by $C 2^{l / 2}$ . Therefore the low-frequency contribution to $∥ f - g ∥_{\infty}$ is at most $C R_{n}^{M} n^{- 1 / 2} \sum_{l \leq j_{n}} 2^{l / 2} w_{l}$ , and the high-frequency contribution is at most $C u_{n} \sum_{l > j_{n}} 2^{- l γ}$ . These series also give uniformly convergent representatives because $γ > 0$ .

2.1step 1.2algebra

Since $w_{l}$ is nondecreasing, $\sum_{l \leq j_{n}} 2^{l / 2} w_{l} \leq C 2^{j_{n} / 2} w_{j_{n}}$ by summing a geometric series. Also $\sum_{l > j_{n}} 2^{- l γ} \leq C_{γ} 2^{- j_{n} γ}$ . The first bound in step 1.2 is thus at most $C R_{n}^{M} w_{j_{n}} 2^{j_{n} / 2} / \sqrt{n} = C R_{n}^{M} u_{n} \sqrt{j_{n}} 2^{j_{n} / 2} / \sqrt{n}$ .

3.1F2step 1.2step 2.1algebra∎

The relation $2^{j_{n}} ≍ (n / \log n)^{1 / (2 γ + 1)}$ implies both $2^{- j_{n} γ} ≍ (n / \log n)^{- γ / (2 γ + 1)}$ and $\sqrt{j_{n}} 2^{j_{n} / 2} / \sqrt{n} \leq C_{γ} (n / \log n)^{- γ / (2 γ + 1)}$ . Combining the low- and high-frequency bounds in steps 1.2 and 2.1 and using $R_{n}^{M} = O_{P} (1)$ from [F2] yields the stated diameter bound.

Depends on

Used by

Type-S and Type-H density credible bands have asymptotically exact coverage Corollary

Dependency tree · two levels

14 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 5, Proposition 5, and proof of §5.4 (standard reference, not scraped)
Giné and Nickl, Mathematical Foundations of Infinite-Dimensional Statistical Models, Corollary 7.3.24 and proof (standard reference, not scraped)