ExampleConstruction: Literature-sourcedVerification: 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.

A power-law truth lies in the polished-tail class

Example

Fix $β > 0$ , $M > 0$ , and $ρ \geq 2$ . Set $θ_{0, 1} = 0$ and $θ_{0, i} = \sqrt{M} i^{- 1 / 2 - β}$ for $i \geq 2$ . Let $N_{0} = 2$ and $L_{0} = (2 β + 1) / (1 - ρ^{- 2 β})$ . Then $θ_{0} \in Θ_{β} (M) \cap Θ_{p t} (L_{0}, N_{0}, ρ)$ . Consequently, under the hypotheses of Conservative coverage of adaptive empirical-Bayes credible balls on polished tails, an admissible sufficiently large inflation gives conservative frequentist coverage tending to one for this truth.

Facts & Assumptions

Given: $β > 0$ , $M > 0$ , $ρ \geq 2$ , and the sequence in the Example.

[F1]

Membership in $Θ_{β} (M)$ means $\sup_{i} i^{1 + 2 β} θ_{i}^{2} \leq M$ . Hyperrectangle classes in a Gaussian sequence model

[F2]

Membership in $Θ_{p t} (L_{0}, N_{0}, ρ)$ means $\sum_{i = N}^{\infty} θ_{i}^{2} \leq L_{0} \sum_{i = N}^{⌊ ρ N ⌋} θ_{i}^{2}$ for every integer $N \geq N_{0}$ . Polished-tail class for a Gaussian sequence

[F3]

For a truth in this polished-tail class with $θ_{0, 1} = 0$ , the source theorem gives an inflation $L$ with frequentist coverage tending to one. Conservative coverage of adaptive empirical-Bayes credible balls on polished tails

Verification

1.1F1givenalgebra

The sequence is square summable because $\sum_{i = 2}^{\infty} i^{- 1 - 2 β} \leq 1 + \int_{1}^{\infty} x^{- 1 - 2 β} d x < \infty$ . For every $i \geq 2$ , $i^{1 + 2 β} θ_{0, i}^{2} = M$ , and the first coordinate is zero. Thus [F1] holds.

1.2F2givenalgebra

For $N \geq 2$ , monotonicity of $x^{- 1 - 2 β}$ gives $\sum_{i = N}^{\infty} i^{- 1 - 2 β} \leq N^{- 1 - 2 β} + \int_{N}^{\infty} x^{- 1 - 2 β} d x \leq (1 + \frac{1}{2 β}) N^{- 2 β}$ and $\sum_{i = N}^{⌊ ρ N ⌋} i^{- 1 - 2 β} \geq \int_{N}^{⌊ ρ N ⌋ + 1} x^{- 1 - 2 β} d x \geq \frac{1 - ρ^{- 2 β}}{2 β} N^{- 2 β} .$ Multiplying by $M$ shows that the tail-to-block ratio is at most $(2 β + 1) / (1 - ρ^{- 2 β}) = L_{0}$ , so [F2] holds.

2.1F3step 1.2∎

The truth has $θ_{0, 1} = 0$ and satisfies [F2], so the theorem [F3] supplies a sufficiently large inflation for which its frequentist coverage tends to one.

Depends on

Used by

Nothing in the library uses this result yet.

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

Botond Szabó, Aad van der Vaart and Harry van Zanten, Frequentist coverage of adaptive nonparametric Bayesian credible sets, Annals of Statistics 43(4) (2015) (standard reference, not scraped)