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

CDF and multiscale credible-band calibration from weak BvM limits

Statement

Let $P_{0}$ have a density $f_{0}$ on $[0, 1]$ bounded above and bounded away from zero, and put $F_{0} (t) = \int_{0}^{t} f_{0} (x) d x$ . Use the wavelet basis and $M_{0} (w)$ of Little-o multiscale coefficient space M0(w), and assume the wavelet conditions and summability condition $\sum_{l} w_{l} 2^{- l / 2} < \infty$ of The multiscale primitive map is continuous into C[0,1]. Let $T_{n}$ be a measurable $L^{2}$ -valued center, let $Π_{n}$ be a posterior kernel supported on $L^{2}$ densities, and define $Q_{n}$ to be the conditional law on $M_{0} (w)$ of $\sqrt{n} (f - T_{n})$ under $f \sim Π_{n} (\cdot ∣ X^{n})$ .

Assume under $P_{0}^{n}$ that (i) $Q_{n}$ converges in bounded-Lipschitz distance in probability to the centered Gaussian bridge coefficient law $G_{P_{0}}$ in $M_{0} (w)$ , whose finite coefficient covariances are $P_{0} [(h - P_{0} h) (g - P_{0} g)]$ , and (ii) $\sqrt{n} (T_{n} - f_{0}) \Rightarrow G_{P_{0}}$ in $M_{0} (w)$ . For $u = 1 - α$ , let $q_{M}$ and $q_{C}$ be the lower $u$ -quantiles of $∥ G_{P_{0}} ∥_{M (w)}$ and $∥ J G_{P_{0}} ∥_{\infty}$ . Assume both CDFs are continuous on $R$ and strictly increasing on open neighborhoods of their respective quantiles, and that $q_{M}, q_{C} > 0$ . These local quantile conditions allow the CDFs to be constant on the negative half-line. In the projected empirical-center case $T_{n} = P_{n} (L_{n})$ , Projected empirical bridge CLT in the little-o multiscale space supplies premise (ii) under its stated smoothness and cutoff conditions. For the source-specific type-S and type-H priors, the posterior BvM premise (i) is established in Type-S density posteriors satisfy the weak multiscale Bernstein–von Mises theorem and Type-H histogram posterior weak Bernstein–von Mises theorem, respectively.

For a posterior draw $f$ , write $F_{f} = J f$ and $F_{T_{n}} = J T_{n}$ , where $J$ is the primitive map of The multiscale primitive map is continuous into C[0,1]. Then 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 $B_{P_{0}} (t)$ , with covariance $F_{0} (s \land t) - F_{0} (s) F_{0} (t)$ .

For $0 < α < 1$ , let $R_{n}^{M}$ and $R_{n}^{C}$ be the posterior lower $1 - α$ quantiles of $∥ \sqrt{n} (f - T_{n}) ∥_{M (w)}$ and $∥ \sqrt{n} (F_{f} - F_{T_{n}}) ∥_{\infty}$ , respectively. The corresponding posterior balls $C_{n}^{M} = {f : ∥ f - T_{n} ∥_{M (w)} \leq R_{n}^{M} / \sqrt{n}}, C_{n}^{C} = {F : ∥ F - F_{T_{n}} ∥_{\infty} \leq R_{n}^{C} / \sqrt{n}}$ are measurable credible sets of posterior mass at least $1 - α$ . Their frequentist coverage tends to $1 - α$ , and the scaled radii converge to the respective $1 - α$ quantiles of $∥ G_{P_{0}} ∥_{M (w)}$ and $∥ B_{P_{0}} ∥_{\infty}$ .

Facts & Assumptions

Given: The density law, posterior kernel, wavelet basis, space $M_{0} (w)$ , primitive map, two weak-convergence assumptions, continuous strictly increasing limit norm CDFs, and $0 < α < 1$ in the Statement.

[F1]

Little-o multiscale coefficient space M0(w): $M_{0} (w)$ has the weighted supremum norm on wavelet coefficients whose normalized level maxima vanish.

[F2]

The multiscale coefficient space is separable and has vanishing projection tails: every square-summable wavelet coefficient sequence belongs to $M_{0} (w)$ .

[F3]

The multiscale primitive map is continuous into C[0,1]: $J : M_{0} (w) \to C ([0, 1])$ is continuous and agrees with $f \mapsto (t \mapsto \int_{0}^{t} f)$ for $L^{2}$ functions.

[F4]

Continuous mapping theorem: a continuous map carries weak convergence of probability laws to weak convergence of their pushforwards.

[F5]

Posterior quantiles are measurable and bracket their probability level: for a posterior probability kernel on $R$ , its lower $u$ -quantile is measurable and its CDF brackets $u$ .

[F6]

Posterior quantiles stabilize under scalar weak convergence: if the limiting scalar CDF is continuous on $R$ and strictly increasing on a neighborhood of the target quantile, bounded-Lipschitz convergence in probability implies convergence of that posterior quantile.

[F7]

Posterior credible set: a graph-measurable rule whose posterior mass is at least $1 - α$ is a posterior credible set at level $1 - α$ .

[A1]

The posterior laws $Q_{n}$ converge in bounded-Lipschitz distance in probability to the centered Gaussian bridge coefficient law $G_{P_{0}}$ in $M_{0} (w)$ .

[A2]

The sampling centers satisfy $\sqrt{n} (T_{n} - f_{0}) \Rightarrow G_{P_{0}}$ in $M_{0} (w)$ .

[A3]

The CDFs of $∥ G_{P_{0}} ∥_{M (w)}$ and $∥ J G_{P_{0}} ∥_{\infty}$ are continuous on $R$ and strictly increasing on open neighborhoods of their positive $1 - α$ quantiles. Continuity at each lower quantile $q$ implies its CDF value is $1 - α$ .

[F8]

Portmanteau theorem: weak convergence of probability measures gives convergence of probabilities of sets whose boundary has zero limit measure.

[F9]

Projected empirical bridge CLT in the little-o multiscale space: for the projected empirical center and the theorem's coefficient regularity and cutoff assumptions, $\sqrt{n} (P_{n} (L_{n}) - f_{0}) \Rightarrow G_{P_{0}}$ in $M_{0} (w)$ .

[F11]

Logarithmic negative Sobolev spaces for white noise: the wavelets form a complete orthonormal basis of $L^{2} ([0, 1])$ , so finite orthogonal projections converge in $L^{2}$ .

[F12]

Cauchy-Schwarz for random variables: square-integrable random variables satisfy $∣ E [U V] ∣ \leq (E U^{2} E V^{2})^{1 / 2}$ .

Proof

1.1A1F3F11F12givenalgebra

The posterior draw $f$ and center $T_{n}$ are $L^{2}$ -valued, so [F2] embeds $\sqrt{n} (f - T_{n})$ in $M_{0} (w)$ ; [F1] supplies its norm. For an $L$ -Lipschitz map $T$ between metric spaces and any admissible bounded 1-Lipschitz test $h$ on its target, $h \circ T / \max (1, L)$ is an admissible test on its domain. Therefore $β_{B L} (T_{#} ν, T_{#} ρ) \leq \max (1, L) β_{B L} (ν, ρ) .$ By [F3], $J$ is linear and Lipschitz with a finite constant $L_{J}$ . The bound applied pointwise to the data-indexed laws in [A1] gives $β_{B L} (J_{#} Q_{n}, J_{#} G_{P_{0}}) \to 0$ in probability. Moreover, if $ℓ : C ([0, 1]) \to R$ is continuous and linear, then $ℓ \circ J$ is continuous and linear on $M_{0} (w)$ . The centered Gaussian premise on $G_{P_{0}}$ says exactly that this scalar pushforward is centered normal, allowing zero variance. Thus $J_{#} G_{P_{0}}$ is a centered Gaussian Borel law. In particular, for any finite $t_{1}, \dots, t_{m}$ and real $a_{1}, \dots, a_{m}$ , the functional $x \mapsto \sum_{i} a_{i} J x (t_{i})$ is continuous and linear, so the evaluation vector $(J G_{P_{0}} (t_{i}))_{i = 1}^{m}$ is jointly centered Gaussian. This uses only the scalar Gaussian pushforward meaning of the premise, without characteristic-function uniqueness or a Gaussian existence theorem. To identify its covariance, let $p_{J} 1_{[0, s]}$ be the finite wavelet projection of the indicator. The finite Gaussian coefficient covariance gives $Cov (J (P_{J} G_{P_{0}}) (s), J (P_{J} G_{P_{0}}) (t)) = P_{0} [(p_{J} 1_{[0, s]} - P_{0} p_{J} 1_{[0, s]}) (p_{J} 1_{[0, t]} - P_{0} p_{J} 1_{[0, t]})] .$ By [F11], $p_{J} 1_{[0, s]} \to 1_{[0, s]}$ in Lebesgue $L^{2}$ ; since $f_{0} \leq B$ , this is also convergence in $L^{2} (P_{0})$ . The variance of a difference of two finite projected Gaussian evaluations is the $P_{0}$ -variance of the corresponding difference of projected indicators, so it tends to zero; hence those evaluations are Cauchy in $L^{2}$ . They also converge almost surely to $J G_{P_{0}} (s)$ because $P_{J} G_{P_{0}} \to G_{P_{0}}$ in $M_{0} (w)$ and $J$ is continuous. The almost-sure and in-probability limits coincide: for any $ε > 0$ , the probability that they differ by more than $ε$ is bounded by the two probabilities that each sequence differs from its limit by more than $ε / 2$ , both tending to zero. If $U_{J}, V_{J}$ are the projected evaluations and $U, V$ their $L^{2}$ limits, [F12] gives $∣ E [U_{J} V_{J}] - E [U V] ∣ \leq ∥ U_{J} - U ∥_{2} ∥ V_{J} ∥_{2} + ∥ U ∥_{2} ∥ V_{J} - V ∥_{2} ⟶ 0;$ the norms $∥ V_{J} ∥_{2}$ are bounded because $V_{J} \to V$ in $L^{2}$ , and the means converge to zero as well. Thus the finite covariance passes to the limit. The resulting covariance is $P_{0} [(1_{[0, s]} - F_{0} (s)) (1_{[0, t]} - F_{0} (t))] = F_{0} (s \land t) - F_{0} (s) F_{0} (t)$ , the defining covariance of the $P_{0}$ -Brownian bridge.

1.2F5F7givenalgebra

The posterior pushforward under either norm is a probability kernel on $[0, \infty)$ . By [F5], the two lower quantiles are measurable and their posterior CDFs at those radii are at least $1 - α$ . Since the centers and norms are measurable, the membership graphs of $C_{n}^{M}$ and $C_{n}^{C}$ are measurable. Thus both sets are credible by [F7].

2.1A1A2A3F1F6F9step 1.1

The norm maps $x \mapsto ∥ x ∥_{M (w)}$ and $F \mapsto ∥ F ∥_{\infty}$ are 1-Lipschitz by the reverse triangle inequality. Applying the pushforward bound of step 1.1 first to the $M (w)$ norm and then to the supremum norm after $J$ gives bounded-Lipschitz convergence in probability of both posterior norm laws to their corresponding limit norm laws. Their CDFs satisfy [A3], so [F6] gives $R_{n}^{M} \to q_{M}$ and $R_{n}^{C} \to q_{C}$ in probability. For the projected empirical center $T_{n} = P_{n} (L_{n})$ , [F9] verifies [A2] under the smoothness and cutoff assumptions in [F9].

3.1A2A3F3F4F8step 2.1algebra∎

By [A2] and [F4], $\sqrt{n} (T_{n} - f_{0}) \Rightarrow G_{P_{0}}$ and its primitive converges weakly to $B_{P_{0}}$ . The frequentist error uses the negative center difference, but $∥ f_{0} - T_{n} ∥_{M (w)} = ∥ T_{n} - f_{0} ∥_{M (w)}$ and $∥ J (f_{0} - T_{n}) ∥_{\infty} = ∥ J (T_{n} - f_{0}) ∥_{\infty}$ because $J$ is linear. Thus each scaled frequentist error norm converges to the corresponding limit norm in [A3]. On the event that the random radius is within $ε$ of its deterministic limit from step 2.1, coverage is bounded above and below by probabilities for the frequentist norm with fixed thresholds expanded or contracted by $ε$ . [F8] gives convergence of those fixed-threshold probabilities because [A3] makes their boundary probabilities zero. Sending $ε ↓ 0$ and using the CDF value $1 - α$ at its quantile from [A3] yields $1 - α$ for both coverage probabilities. This comparison does not require independence between the data-dependent posterior radii and the frequentist center.

Depends on

Used by

Dependency tree · two levels

61 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 4–5, Corollary 2, and §5.4 (standard reference, not scraped)
Giné and Nickl, Mathematical Foundations of Infinite-Dimensional Statistical Models, Theorem 7.3.23 and proof (standard reference, not scraped)