CorollaryStatement: 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.

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

Statement

Assume AC. Use either Type-S1, Type-S2 or Type-H with all the truth, basis, prior-scale, Dirichlet-parameter and cutoff conditions of Type-S log-density and type-H histogram prior families. Let $w_{l} \geq 1$ be nondecreasing, $w_{l} / \sqrt{l + 1} \to \infty$ , and $\sum_{l} w_{l} 2^{- l / 2} < \infty$ . In Type S take $T_{n} = P_{n} (L_{n})$ , the empirical wavelet projection through level $L_{n}$ . In Type H take the empirical histogram $T_{n} = h_{n}$ at mesh $2^{- L_{n}}$ , equivalently the Haar projection with scaling coordinate and details $l < L_{n}$ .

For each $0 < η < 1$ , the posterior multiscale and CDF balls of CDF and multiscale credible-band calibration from weak BvM limits, at posterior level $1 - η$ and centered at these $T_{n}$ , have posterior mass at least $1 - η$ and frequentist coverage tending to $1 - η$ . Their scaled radii converge in probability to the positive finite $1 - η$ quantiles of the corresponding Gaussian bridge norms. In particular, writing $F_{h} (t) = \int_{0}^{t} h (x) d x$ , the posterior law of $\sqrt{n} (F_{f} - F_{T_{n}})$ converges in bounded-Lipschitz distance on $C ([0, 1])$ to the $P_{0}$ -Brownian bridge law, in $P_{0}^{n}$ -probability.

If additionally the coefficient smoothness and undersmoothing hypotheses of Diameter of undersmoothed multiscale credible bands hold, its intersection with the stated coefficient smoothness ball has the same limiting coverage and the diameter bound asserted there. No unverified entropy, prior-mass, posterior contraction or quantile-regularity premise is required in this corollary.

Facts & Assumptions

Given: AC, one of the three source-specific prior regimes, the specified empirical center, admissible summable weights, and $0 < η < 1$ .

[A1]

The Axiom of Choice is inherited from the following suppliers.

[F1]

Type-S density posteriors satisfy the weak multiscale Bernstein–von Mises theorem and Type-H histogram posterior weak Bernstein–von Mises theorem prove posterior bounded-Lipschitz convergence about the respective empirical projections, to the Borel Gaussian bridge with covariance $P_{0} [(ψ - P_{0} ψ) (ψ^{'} - P_{0} ψ^{'})]$ .

[F2]

Compact wavelet projections approximate smooth functions and commute asymptotically with multiplication preserves coefficient regularity of $e^{g}$ at every positive order, including integers. Projected empirical bridge CLT in the little-o multiscale space proves the sampling CLT for bounded truths with coefficient smoothness $γ > 1 / 2$ and either cutoff regime.

[F3]

Continuous and strictly increasing norm distributions for density bridges proves that both bridge norm CDFs are continuous and strictly increasing on positive arguments and have unique positive finite interior quantiles, under the given positive bounded truth and primitive-map summability conditions.

[F4]

CDF and multiscale credible-band calibration from weak BvM limits gives measurable credible balls, CDF pushforward convergence, radius limits and exact asymptotic coverage from posterior BvM, the sampling-center CLT and the stated norm-quantile conditions.

[F5]

Diameter of undersmoothed multiscale credible bands gives the additional smoothness-ball coverage and diameter conclusion under its explicit coefficient smoothness and undersmoothing assumptions.

Proof

1.1A1F1F2givenalgebra

In Type S, [F1] proves posterior BvM about $T_{n} = P_{n} (L_{n})$ with the locally proved S1 range $α > 1$ and Gaussian S2 range $α > 1 / 2$ , $0 < r < α - 1 / 4$ . The truth $g_{0} = \log f_{0}$ has $α$ coefficient regularity, so [F2] gives that regularity for $f_{0} = e^{g_{0}}$ as well. The retained basis has the support, overlap and supremum bounds required by the empirical-process theorem in [F2]. Taking $γ = α > 1 / 2$ and the given cutoff therefore proves its sampling-center CLT with the same Gaussian bridge.

1.2F1F2givenalgebra

In Type H, [F1] proves posterior BvM about the empirical histogram $h_{n}$ . Haar wavelets have the same support, overlap and supremum bounds. The ordinary $α$ -Hölder truth, $1 / 2 < α \leq 1$ , has Haar coefficients bounded by $C 2^{- l (α + 1 / 2)}$ : subtract its value at one point of the support in the coefficient integral, use the zero mean, support diameter $2^{- l}$ and $L^{1}$ norm $2^{- l / 2}$ . The histogram projection retains details through $J_{n} = L_{n} - 1$ . Both given cutoff regimes remain true with this $J_{n}$ , since multiplying $2^{L_{n}}$ by $1 / 2$ changes only their comparison constants. Thus [F2] with $γ = α$ gives the sampling CLT about this exact histogram center. The finite scaling coordinate is included and its centered fluctuation is zero.

2.1F1F3F4step 1.1step 1.2given

In all three cases, positivity and boundedness of $f_{0}$ , admissibility, and the displayed summability verify [F3]. Hence every norm-quantile assumption of [F4] holds at $u = 1 - η$ . Steps 1.1, 1.2 verify its posterior and sampling premises, with the same coefficient covariance law. Applying [F4] proves all asserted CDF limits, measurable credibility, radius limits and frequentist coverage, for the exact empirical centers and every $0 < η < 1$ .

3.1F5step 2.1given∎

When the additional hypotheses in the last paragraph of the Statement hold, the multiscale credible ball just obtained is precisely the input to [F5]. Applying that theorem yields its smoothness-intersection coverage and stated diameter rate. These are additional hypotheses only for this diameter conclusion; the coverage and CDF conclusions in step 2.1 required no such extra conditions.

Depends on

Used by

Uniform truth under type-S and type-H density priors Example

Dependency tree · two levels

51 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, Theorems 3–5 (standard reference, not scraped)