ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

The IID bootstrap for a smooth mean functional

Example

Let $X_{1}, X_{2}, \dots$ be IID real random variables with mean $μ$ and variance $0 < σ^{2} < \infty$ , and estimate $θ = μ$ by the sample mean. This is the smooth statistic $g (x) = x$ in the theorem.

Facts & Assumptions

Given: The IID sample, finite positive variance, and ideal empirical bootstrap.

[A1]

AC is assumed as required by the multivariate and conditional IID CLTs used below. The Axiom of Choice

[F1]

For a Borel $g$ , the estimator is $g ({\overset{ˉ}{X}}_{n})$ and the bootstrap estimator is $g ({\overset{ˉ}{X}}_{n}^{*})$ . IID empirical bootstrap sample and mean statistic

[F2]

Under the stated moment and differentiability hypotheses, the centered sample and bootstrap roots have the same $N (0, σ^{2})$ first-order limit. First-order IID bootstrap validity for smooth functions of a mean

Verification

1.1A1F1given

Here $g (x) = x$ is Borel and differentiable everywhere with derivative $a = 1$ . Thus $a^{T} Σ a = Var (X_{1}) = σ^{2} \in (0, \infty)$ , so all assumptions of [F2] hold.

2.1A1F2step 1.1∎

Since ${\hat{θ}}_{n} = {\overset{ˉ}{X}}_{n}$ and ${\hat{θ}}_{n}^{*} = {\overset{ˉ}{X}}_{n}^{*}$ by [F1], [F2] gives $\sqrt{n} ({\overset{ˉ}{X}}_{n} - μ) \Rightarrow N (0, σ^{2})$ and the conditional law of $\sqrt{n} ({\overset{ˉ}{X}}_{n}^{*} - {\overset{ˉ}{X}}_{n})$ converges weakly in probability to the same normal law. This is first-order distributional validity only.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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

University of Washington STAT 581, Chapter 8: Bootstrap and Jackknife Estimation of Sampling Distributions, §4 (standard reference, not scraped)