ExampleConstruction: AI-adaptedVerification: 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.

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

Example

The uniform truth $f_{0} = 1$ meets the truth-side smoothness and positive-bound conditions for both a type-S log-density prior and a type-H dyadic histogram prior. The weight sequence $w_{l} = \max (1, \sqrt{l} \log (l + 1))$ is admissible and also satisfies the extra summability needed for the CDF map. Thus the source-specific posterior BvM and credible-band conclusions of Type-S and Type-H density credible bands have asymptotically exact coverage apply to these choices.

Facts & Assumptions

Given: The type-S/type-H definitions of Type-S log-density and type-H histogram prior families and the admissible multiscale space of Little-o multiscale coefficient space M0(w).

[F1]

Type-S log-density and type-H histogram prior families: both families require a density bounded above and bounded away from zero; type S1 requires $\log f_{0} \in C_{ψ}^{α}$ with $α > 1$ , type S2 uses $α > 1 / 2$ and $0 < r < α - 1 / 4$ , while type H requires $f_{0} \in C_{ψ}^{α}$ for $1 / 2 < α \leq 1$ and the displayed Dirichlet-parameter bounds.

[F2]

Little-o multiscale coefficient space M0(w): admissibility means $w_{l} / \sqrt{l} \to \infty$ .

[F3]

Type-S and Type-H density credible bands have asymptotically exact coverage: the specified prior regimes, truth bounds and admissible summable weights imply posterior weak BvM and asymptotically exact multiscale and CDF credible-band coverage.

Verification

Given: The prior families and $f_{0} (x) = 1$ on $[0, 1]$ .

1.1F1givenalgebra

Since $\log f_{0} = 0$ and $f_{0} = 1$ , its wavelet coefficient smoothness norm is finite at every order and it is bounded above and away from zero. For type S1 choose $α = 2$ and the Laplace density $φ_{H} (x) = \frac{1}{2} e^{- ∣ x ∣}$ , whose logarithm is Lipschitz; its scales are $2^{- l (2 + 1 / 2)}$ . For type S2 choose $α = 2$ and $r = 1$ , which satisfies $0 < 1 < 2 - 1 / 4$ .

1.2F1givenalgebra

For type H choose truth smoothness $α = 1$ , hyperparameters $a = c_{1} = c_{2} = 1$ , and $a_{k, L} = 1$ for every cell. Then $2^{- L} \leq a_{k, L} \leq 1$ , and the uniform truth belongs to $C_{ψ}^{1}$ .

2.1F2F3step 1.1step 1.2givenalgebra∎

The sequence $w_{l} = \max (1, \sqrt{l} \log (l + 1))$ is nondecreasing, since both entries in the maximum are nondecreasing for $l \geq 1$ . It satisfies $w_{l} / \sqrt{l} \to \infty$ . Also $\sum_{l} w_{l} 2^{- l / 2} < \infty$ because the ratio of successive terms $\sqrt{l} \log (l + 1) 2^{- l / 2}$ tends to $2^{- 1 / 2} < 1$ . Thus it is admissible and meets the CDF primitive summability condition. Steps 1.1–1.2 verify every regime and truth premise of [F3], so its posterior BvM and credible-band conclusions apply to these examples.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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, §3.2 (standard reference, not scraped)