ExampleConstruction: AI-adaptedVerification: AI-generatedPipeline-generatedprecheck pass

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.

Weakly close root laws can still give failed uniform coverage

Example

Assume AC and let $n \geq 1$ . Let $P = {Bernoulli (p) : 0 \leq p \leq 1}$ , and use the sample mean with root $R_{n, p} = \sqrt{n} ({\overset{ˉ}{X}}_{n} - p)$ . Under the ordinary bootstrap, the conditional root law is the conditional law of $R_{n, p}^{*} = \sqrt{n} ({\overset{ˉ}{X}}_{n}^{*} - {\overset{ˉ}{X}}_{n})$ given the observed sample; write $L^{*}$ for this law and $L$ for the sampling law. For every $ϵ > 0$ , $\sup_{p \in [0, 1]} P_{p} ⁣ (π (L^{*} (R_{n, p}^{*}), L (R_{n, p})) > ϵ) ⟶ 0,$ so the root laws are uniformly close in a metric for weak convergence. Nevertheless, for any fixed $λ > 0$ and $α \in (0, e^{- λ})$ , the one-sided bootstrap lower confidence set based on the $(1 - α)$ -quantile has coverage below $1 - α$ along $p_{n} = 1 - λ / n$ . Thus weak-metric closeness alone does not ensure uniform quantile coverage.

Facts & Assumptions

Given: AC, the Bernoulli model class, the sample-mean estimator, the ordinary bootstrap root, and the generalized quantile convention from CDF ordering and uniform error control quantile coverage.

[A1]

The Axiom of Choice: AC is the assertion that every family of nonempty sets has a choice function.

[F1]

m-out-of-n bootstrap and subsampling: The ordinary bootstrap draws a size- $n$ sample conditionally IID from $P_{n}$ and centers the resampled statistic at ${\hat{θ}}_{n}$ .

[F2]

Identical distribution and IID families: The original observations are mutually independent and have one common law.

[F3]

Partial sums, row sums and sample means: ${\overset{ˉ}{X}}_{n} = n^{- 1} \sum_{i = 1}^{n} X_{i}$ .

[F4]

Bernoulli random variables and binomial random variables as sums of independent Bernoulli trials: A Bernoulli $(p)$ variable is $1$ with probability $p$ and $0$ otherwise; a binomial variable is a finite sum of independent Bernoulli variables.

[F5]

A Bernoulli $(p)$ variable has mean $p$ and variance $p (1 - p)$ ; a binomial $(n, p)$ variable has mean $n p$ and variance $n p (1 - p)$ : A binomial $(n, p)$ variable has mean $n p$ and variance $n p (1 - p)$ .

[F6]

Chebyshev's inequality for random variables: For a square-integrable real random variable $Y$ and $t > 0$ , $P (∣ Y - E Y ∣ \geq t) \leq Var (Y) / t^{2}$ .

[F7]

Bernoulli root laws are uniformly close in Levy–Prokhorov distance: For every $n$ and $p, q \in [0, 1]$ , $π (μ_{n, p}, μ_{n, q}) \leq ∣ p - q ∣^{1 / 3}$ for the centered, $\sqrt{n}$ -scaled Bernoulli sample-mean roots.

[F8]

Confidence sets and coverage: A confidence procedure has measurable membership sections, and its coverage at a fixed parameter is the probability that the procedure contains that parameter.

[F9]

Levy prokhorov metric: $π$ is the infimum of radii satisfying the two closed-set enlargement inequalities in the statement of the definition.

[F10]

Weak convergence of borel probability measures: Weak convergence of Borel laws means convergence of integrals against all bounded continuous real functions.

[F11]

Levy prokhorov metric metrizes weak convergence: Under AC, convergence in Levy–Prokhorov distance on a separable metric space is equivalent to weak convergence of Borel probability laws.

[F12]

Uniform subsampling coverage under root-law control: Uniform quantile coverage follows from the stated one-sided root-CDF comparisons and uniform feasible-root CDF control; a weak metric alone is not among those premises.

[F13]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: For $x > 0$ , $\log^{'} (x) = 1 / x$ and $\log x = \int_{1}^{x} d t / t$ .

[F14]

CDF ordering and uniform error control quantile coverage: The generalized quantile is $q_{G} (u) = \inf {x : G (x) \geq u}$ for $u \in (0, 1)$ , with $q_{G} (0) = - \infty$ and $q_{G} (1) = + \infty$ .

[F15]

The Euclidean metric space $R$ is separable because $Q$ is countable and dense in $R$ . Separability: the existence of an at most countable dense subset $Q$ is countably infinite Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable

Verification

1.1F1F2F3F4F7

Under $P_{p}$ , ${\overset{ˉ}{X}}_{n}$ has law $Binomial (n, p) / n$ . Conditional on the sample, the bootstrap observations are IID Bernoulli $({\overset{ˉ}{X}}_{n})$ , so their centered root law is $μ_{n, {\overset{ˉ}{X}}_{n}}$ , while the true root law is $μ_{n, p}$ . By [F7], $π (L^{*} (R_{n, p}^{*}), L (R_{n, p})) \leq ∣ {\overset{ˉ}{X}}_{n} - p ∣^{1 / 3}$ .

1.2F1F3F8

Fix $λ > 0$ , take $p_{n} = 1 - λ / n$ for $n > λ$ , and let $q_{n}$ be the conditional $(1 - α)$ -quantile of $R_{n, p_{n}}^{*}$ . Define the lower interval $I_{n} = [{\overset{ˉ}{X}}_{n} - q_{n} / \sqrt{n}, 1] \cap [0, 1]$ . It is measurable because the data take only finitely many values, and $p_{n} \in I_{n}$ is exactly the coverage event for root threshold $q_{n}$ .

2.1A1F5F6F9F10F11F15step 1.1algebra

From [F5], ${Var}_{p} ({\overset{ˉ}{X}}_{n}) = p (1 - p) / n \leq 1 / (4 n)$ . For each $ϵ > 0$ , Chebyshev's inequality [F6] and step 1.1 give $\sup_{p \in [0, 1]} P_{p} {π (L^{*} (R_{n, p}^{*}), L (R_{n, p})) > ϵ} \leq \sup_{p} P_{p} {∣ {\overset{ˉ}{X}}_{n} - p ∣ > ϵ^{3}} \leq 1 / (4 n ϵ^{6}) \to 0$ . By [F15], $R$ is a separable metric space, so [F11] shows this is uniform closeness in a metric that induces weak convergence.

2.2F1F13F14step 1.2algebra

On the event $X_{1} = \dots = X_{n} = 1$ , the empirical law is $δ_{1}$ , every bootstrap root is zero, and [F14] gives $q_{n} = 0$ because $1 - α \in (0, 1)$ ; then $I_{n} = {1}$ and $p_{n} \notin I_{n}$ . This event has probability $p_{n}^{n} = (1 - λ / n)^{n}$ . By the integral formula in [F13], $n \log (1 - λ / n) = - n \int_{1 - λ / n}^{1} d t / t \to - λ$ , since the integrand converges uniformly to $1$ on that shrinking interval; exponentiating gives $p_{n}^{n} \to e^{- λ}$ . Hence ${lim sup}_{n} P_{p_{n}} (p_{n} \in I_{n}) \leq 1 - e^{- λ} < 1 - α$ , so ${lim inf}_{n} \inf_{p \in [0, 1]} P_{p} (p \in I_{n}) < 1 - α$ .

3.1A1F7F11F12step 1.1step 2.1step 1.2step 2.2∎

Steps 1.1 and 2.1 establish uniform weak-metric closeness, while steps 1.2 and 2.2 show the coverage failure. Thus weak-metric closeness alone does not imply uniform quantile coverage or the stronger root-CDF and feasible-root conditions in [F12]. The coupling and coverage calculation use no choice; AC enters only through the metric-to-weak-topology equivalence [F11].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

84 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

J. P. Romano and A. M. Shaikh, On the Uniform Asymptotic Validity of Subsampling and the Bootstrap, §2.2, Remark 2.7 and Example 2.1 (standard reference, not scraped)