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.
Exact adaptive credible coverage by posterior-null deletion
Example
Assume AC and Countable Choice. Fix , , , , , an integer , , , and . Let a known positive singular-value sequence satisfy , and observe for , where the fixed truth and the are independent variables. For , use the product prior and its product Gaussian posterior with coordinate mean and variance . Select as a Borel global maximizer over of the marginal log-likelihood score assuming the score series is finite on a Borel data domain of probability one for the truths below and is upper semicontinuous in there. The branch uses the whole space and asserts no posterior probability on .
For , write . For , define , with .
For , let and let consist of those satisfying for every integer . Put and assume the fixed constants make each nonempty. There exists a single graph-measurable data-indexed set rule , depending only on the known model and class constants and not on or , such that on it has posterior mass , its uniform frequentist coverage satisfies and its -diameter has the no-log rate uniformly in the following sense: for every there is such that
Example references
Uniform conservative coverage of an inflated empirical-Bayes ball
The lower-selector bracket used in the diameter proof
Szabó, van der Vaart and van Zanten (2015), Theorem 3.6 and §5. The null-deletion construction is a local consequence for the unrestricted set-rule formulation; it is not attributed to that paper.
Facts & Assumptions
Given: Exactly the original question's model, constants, score domain and selector, posterior, nonempty classes , AC and Countable Choice. No change in the permitted set geometry is made.
AC and Countable Choice are assumed as stated. The Axiom of Choice, The Axiom of Countable Choice ()
The procedure and posterior formula give the coordinate means and variances. Empirical-Bayes credible-ball procedure in the inverse Gaussian sequence model, Posterior and marginal-likelihood formulas for the Gaussian sequence prior
For fixed cap , a constant inflation gives coverage tending uniformly to one over polished-tail truths with first coordinate zero, with the whole-space convention at selector zero. Conservative coverage of adaptive empirical-Bayes credible balls on polished tails
The lower-selector bracket holds uniformly over all square-summable truths, with the score normalization and threshold stated there. Marginal-likelihood maximizer bracket on polished tails Its score hypotheses and uniform probability bound are supplied by Uniform marginal-score bounds by derivative integration.
Credibility means graph-measurable membership and posterior mass at least on the declared domain; coverage is fixed-truth sampling probability. Posterior credibility and frequentist coverage
The polished-tail condition is the fixed tail-to-block energy inequality in the Example. Polished-tail class for a Gaussian sequence
Verification
Given: The complete model, class constants, supplied score domain and selector, and quantified conclusions in the Example and Facts & Assumptions. The sequence coordinates are exactly , as in the displayed model and norm; thus here means . No coordinate zero is added to that model.
Fix the inflation in [F2], depending only on the known constants. Let , including its whole-space zero-selector branch. With , [F2] gives . This is uniform because is a subset of the single polished-tail class in that theorem. This step claims conservative coverage only.
The random positive-selector posterior is supported on on a single Borel domain, not merely on a separate almost-sure domain for each fixed hyperparameter. Indeed intersect the supplied score domain with For every square-summable truth the expectation of this nonnegative sum is Thus is Borel and has probability one under every such truth. For every and every , the squared posterior mean is bounded by that same sum, since . For every the variance trace is finite. Hence all positive-parameter posterior laws at these data are supported on , including the selected law. Extend the selector by zero and use the whole space outside this common declared domain. This changes none of the sampling probabilities and asserts no posterior on the zero branch.
We verify the diameter rate uniformly in , rather than import a pointwise Sobolev assertion. Write , , and . In the score of [F3], put , so . For , the multiplier of is at most If , bound both powers and logarithms by their values at ; otherwise use . For , the multiplier is at most The last function of is decreasing for once is uniformly large, since its negative power has exponent at least . Both ranges therefore give These bounds hold simultaneously for , every in the fixed compact interval, and every .
Choose a fixed with . For all sufficiently large , put . For every , step 1.3 makes : here when . Consequently , including the empty-threshold convention . The uniform lower bracket [F3] yields In particular .
Put , and . Define For one may use . The positive-selector posterior's first-coordinate variance is , so it assigns mass zero for every data point of the declared domain, even though the hyperparameter is data-selected. Since , has posterior mass at least ; deleting preserves that mass. On the specified whole-space convention is retained.
Uniformly for , split the posterior variance trace at . Below that cutoff use ; above it use . Summation and an integral comparison give where depends only on the fixed constants (the tail factor is uniformly bounded). Markov's inequality applied to the centered posterior squared norm bounds its norm quantile by . The variances, hence the norm quantile, decrease with by coupling all centered coordinates with the same standard normals. On the event of step 2.1, the selected radius is therefore at most . The derivative of is , so this is at most with one for the full compact interval. Thus outside an event of uniformly vanishing probability, . This includes the uniformly negligible infinite-diameter zero-selector branch.
This is one rule independent of and . Its graph is Borel: the coordinate posterior means and selector are Borel, and the squared norm is the limit of its finite coordinate sums. For completeness, on a fixed countable standard-normal product space the map is nonnegative Borel. Integrating its threshold indicators gives a Borel distribution function in . Its quantile is Borel, by taking the infimum of positive rational radii whose distribution function is at least ; right continuity ensures this quantile has the required posterior mass. The centered norm has a positive finite quantile: it is finite by its finite second moment and has no atom at zero because its first coordinate is nondegenerate. Thus the radius is positive. Deleting the closed codimension-one hyperplane leaves a dense subset of any positive-radius ball: perturb a point toward the center if necessary and then a sufficiently small amount along the first coordinate. Hence has the same diameter as . Diameter is consequently an extended Borel random variable, equal to this expression off and infinity on .
Every allowed truth lies in and has exactly, since . Its coverage equals Subtracting leaves Its absolute value is at most uniformly over both suprema in the question. No independence among , the selector and is used. Also on every branch, so step 3.1 proves the requested diameter statement, in fact with limiting supremum zero for one sufficiently large fixed diameter constant. The nonzero lower norm bound is retained and needs no additional argument. This answers the unchanged unrestricted existence question affirmatively. It does not identify the constructed sets as balls or attribute this null-deletion construction to the cited literature.
Depends on
- Posterior credibility and frequentist coverage
- Empirical-Bayes credible-ball procedure in the inverse Gaussian sequence model
- Posterior and marginal-likelihood formulas for the Gaussian sequence prior
- Marginal-likelihood maximizer bracket on polished tails
- Uniform marginal-score bounds by derivative integration
- Conservative coverage of adaptive empirical-Bayes credible balls on polished tails
- Polished-tail class for a Gaussian sequence
- The Axiom of Choice
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
27 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
- Szabó, van der Vaart and van Zanten, Frequentist coverage of adaptive nonparametric Bayesian credible sets (2015) (standard reference, not scraped)