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

Marginal-likelihood maximizer bracket on polished tails

Statement

Use the inverse Gaussian sequence procedure of Empirical-Bayes credible-ball procedure in the inverse Gaussian sequence model with fixed $p \geq 0$ , $C \geq 1$ , $A > 0$ , and $κ_{i}^{2} \in [C^{- 2} i^{- 2 p}, C^{2} i^{- 2 p}]$ . Fix $L_{0} \geq 1$ , $N_{0} \geq 1$ , and $ρ \geq 2$ . Let $θ_{0} \in Θ_{p t} (L_{0}, N_{0}, ρ)$ with $θ_{0, 1} = 0$ . For $n \geq 3$ and $α \in [0, A]$ , put $N_{n, α} = n^{1 / (1 + 2 α + 2 p)}, h_{n} (α; θ_{0}) = \frac{1 + 2 α + 2 p}{N_{n, α} \log n} \sum_{i = 1}^{\infty} \frac{n^{2} i^{1 + 2 α} (\log i) θ_{0, i}^{2}}{(i^{1 + 2 α + 2 p} + n)^{2}} .$ Define ${\underline{α}}_{n} = \inf {α \in [0, A] : h_{n} (α; θ_{0}) \geq (16 C^{8})^{- 1}}, {\overline{α}}_{n} = \sup {α \in [0, A] : h_{n} (α; θ_{0}) \leq 8 C^{8}},$ with the source conventions $\inf \emptyset = A$ and $\sup \emptyset = 0$ . Then the source bracket result is $\inf_{θ_{0} \in Θ_{p t} (L_{0}, N_{0}, ρ), θ_{0, 1} = 0} P_{θ_{0}}^{(n)} ({\underline{α}}_{n} \leq {\hat{α}}_{n} \leq {\overline{α}}_{n}) ⟶ 1.$ More generally, the same conclusion holds with $A = A_{n}$ whenever $0 < A_{n} \leq \frac{\sqrt{\log n}}{4 \sqrt{\log (ρ \lor e)}}$ for all sufficiently large $n$ . Uniformly in the polished-tail class, for all sufficiently large $n$ , $\frac{n^{- 2 {\underline{α}}_{n} / (1 + 2 {\underline{α}}_{n} + 2 p)}}{n^{- 2 {\overline{α}}_{n} / (1 + 2 {\overline{α}}_{n} + 2 p)}} \leq {[128 C^{16} {4 + 36 L_{0} ρ^{1 + 2 A_{n}}}]}^{1 + 2 p} .$ In particular, for fixed $A$ the two rates are uniformly comparable. The lower bracket alone is valid uniformly over arbitrary $θ_{0} \in ℓ^{2}$ , using the same definition of ${\underline{α}}_{n}$ and the same procedure/domain hypotheses: $\inf_{θ_{0} \in ℓ^{2}} P_{θ_{0}}^{(n)} ({\underline{α}}_{n} \leq {\hat{α}}_{n}) ⟶ 1.$

Facts & Assumptions

Given: The model, thresholds and hypotheses of the Statement.

[F1]

The procedure supplies a measurable global maximizer and the specified endpoint likelihood. Empirical-Bayes credible-ball procedure in the inverse Gaussian sequence model

[F2]

The continuous score, its expectation inequalities, uniform centered-score bounds and polished-tail kernel comparison hold as stated in Uniform marginal-score bounds by derivative integration.

Proof

1.1F2givenalgebra

Set $u = (16 C^{8})^{- 1}$ and $v = 8 C^{8}$ . Continuity of $h_{n}$ implies $h_{n} \leq u$ on $[0, {\underline{α}}_{n}]$ whenever ${\underline{α}}_{n} > 0$ , and $h_{n} \geq v$ on $[{\overline{α}}_{n}, A]$ whenever ${\overline{α}}_{n} < A$ . These implications include the empty-set conventions. Moreover ${\underline{α}}_{n} \leq {\overline{α}}_{n}$ : otherwise any point strictly between them would have $h_{n} < u$ by the first-infimum definition and $h_{n} > v$ by the last-supremum definition, a contradiction. At a nontrivial threshold, continuity gives $h_{n} ({\underline{α}}_{n}) \geq u$ if ${\underline{α}}_{n} < A$ and $h_{n} ({\overline{α}}_{n}) \leq v$ if ${\overline{α}}_{n} > 0$ .

2.1F1F2step 1.1algebra

Write $V_{α} = N_{n, α} \log N_{n, α}$ . The expectation bounds in F2 imply $E M_{n} / V_{α} \geq 1 / (16 C^{4})$ when $h_{n} \leq u$ , and $E M_{n} / (V_{α} h_{n}) \leq - 5 / (8 C^{4})$ when $h_{n} \geq v$ . Therefore $E M_{n} / [V_{α} (1 + h_{n})]$ has a positive margin at least $1 / (32 C^{4})$ on the lower interval and a negative margin of magnitude at least $1 / (32 C^{4})$ on the upper interval. For a nonnegative variable $Y$ , integrating $ε 1_{{Y > ε}} \leq Y$ proves $P (Y > ε) \leq E Y / ε$ . The uniform centered-score bound and this inequality show that, uniformly in polished-tail truths, with probability tending to one the likelihood derivative is positive throughout the lower interval and negative throughout the upper interval. Integration shows strict increase and decrease, including comparisons with the interval endpoints. Every global maximizer lies in the asserted bracket, proving the first conclusion.

3.1F1F2step 1.1step 2.1algebra

For an arbitrary square-summable truth with ${\underline{α}}_{n} > 0$ , the lower interval still has $h_{n} \leq u$ . Apply the final, arbitrary-truth bound in F2 to $[0, {\underline{α}}_{n}]$ with $H = u$ . The positive expectation margin $1 / (16 C^{4})$ is unchanged. Markov's inequality makes the derivative positive throughout that interval with probability tending to one uniformly in all such truths. Thus no global maximizer lies below ${\underline{α}}_{n}$ . If this endpoint is zero, the conclusion holds automatically.

4.1F2step 1.1algebra∎

If ${\underline{α}}_{n} = A$ or ${\overline{α}}_{n} = 0$ , their ordering forces equality of both endpoints and the rate ratio is one. Otherwise apply F2's kernel comparison at $a = {\underline{α}}_{n}$ , $b = {\overline{α}}_{n}$ . Step 1.1 gives $u \leq (4 + 36 L_{0} ρ^{1 + 2 A}) (N_{b} / N_{a}) v$ , hence $N_{a} / N_{b} \leq 128 C^{16} (4 + 36 L_{0} ρ^{1 + 2 A})$ . Finally $n^{- 2 α / (1 + 2 α + 2 p)} = N_{α}^{1 + 2 p} / n$ . Raising the last bound to the power $1 + 2 p$ gives the displayed rate comparison. All constants and probability bounds are uniform in the specified classes.

Depends on

Used by

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

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)
B. T. Knapik, B. Szabó, A. W. van der Vaart and J. H. van Zanten, Bayes procedures for adaptive inference in inverse problems for the white noise model, arXiv:1209.3628 (standard reference, not scraped)