TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Normal sample mean and residual are independent, giving the exact t pivot

Statement

Assume the Axiom of Choice. Use the experiment with data space $(R^{n}, B (R^{n}))$ , parameter set $R \times (0, \infty)$ , and sampling law $P_{μ, σ^{2}} = N (μ, σ^{2})^{\otimes n}$ . Let $n \geq 2$ , $σ > 0$ , and let $X_{1}, \dots, X_{n}$ be the independent coordinates of the observation. Define $\overset{ˉ}{X} = \frac{1}{n} \sum_{i = 1}^{n} X_{i}, S^{2} = \frac{1}{n - 1} \sum_{i = 1}^{n} (X_{i} - \overset{ˉ}{X})^{2}, S = \sqrt{S^{2}} .$ The map $x \mapsto \overset{ˉ}{x}$ is a statistic. The sample mean $\overset{ˉ}{X}$ and residual sum $S^{2}$ are independent, $\frac{(n - 1) S^{2}}{σ^{2}} \sim χ_{n - 1}^{2}, S > 0 almost surely, \tilde{T} : = {\begin{cases} \frac{\overset{ˉ}{X} - μ}{S / \sqrt{n}}, & S > 0, \\ 0, & S = 0 \end{cases} \sim t_{n - 1} .$ For every $0 < α < 1$ , the interval $[\overset{ˉ}{X} - q_{n - 1} (1 - α / 2) \frac{S}{\sqrt{n}}, \overset{ˉ}{X} + q_{n - 1} (1 - α / 2) \frac{S}{\sqrt{n}}]$ has exact coverage $1 - α$ , where $q_{n - 1} (u)$ is the unique $u$ -quantile of $t_{n - 1}$ established in Student t and Fisher F CDFs are continuous and strictly increasing on their supports.

Facts & Assumptions

Given: The Axiom of Choice, $n \geq 2$ , $σ > 0$ , and an independent sample $X_{i} \sim N (μ, σ^{2})$ .

[A1]

The Axiom of Choice is assumed by the normal-law and orthogonal-invariance suppliers. The Axiom of Choice

[A2]

Under the Axiom of Choice, the sequence-selection conclusion of the countable-choice lemma gives Countable Choice, the hypothesis of the continuous-map measurability corollary. The Axiom of Countable Choice ( ${A C}_{ω}$ ) The Axiom of Choice implies countable choice Continuous functions on Euclidean spaces are Borel measurable

[F1]

The law $N (μ, σ^{2})$ is the pushforward of $N (0, 1)$ by the map $z \mapsto μ + σ z$ ; measurable functions of independent random elements remain independent. Standard normal and normal laws Measurable coordinatewise functions preserve independence

[F2]

A statistic is a measurable data map; under Countable Choice, continuous maps between Euclidean spaces are Borel measurable. Statistics and estimators Continuous functions on Euclidean spaces are Borel measurable

[F3]

For $Z \sim N_{n} (0, I_{n})$ and a rank- $r$ orthogonal projection $P$ , $P Z$ and $(I - P) Z$ are independent and their squared norms have laws $χ_{r}^{2}$ and $χ_{n - r}^{2}$ . Orthogonal projections split a standard Gaussian into independent chi-square sums

[F4]

The joint law of independent standard-normal coordinates is $N_{n} (0, I_{n})$ , and each linear projection of that law is normal with the corresponding projected mean and variance. Independent random elements have product joint law Multivariate normal law, including singular covariance

[F5]

Positive-degree chi-square denominators are positive almost surely; $t_{k}$ has a continuous symmetric CDF with unique quantiles, and its law is the piecewise ratio $G / \sqrt{Q_{k} / k}$ set to zero when $Q_{k} = 0$ , for independent $G \sim N (0, 1)$ and $Q_{k} \sim χ_{k}^{2}$ . Positive-degree chi-square laws have a positive density and regular CDF Student t and Fisher F laws Student t and Fisher F CDFs are continuous and strictly increasing on their supports

Proof

Given: The hypotheses in the Statement.

1.1A1A2F1F2F4

By [A2], Countable Choice holds, so [F2] applies to the linear continuous map $x \mapsto \overset{ˉ}{x}$ ; hence it is a statistic on the stated Borel data space. Put $Z_{i} = (X_{i} - μ) / σ$ . The affine pushforward definition in [F1] gives each $Z_{i} \sim N (0, 1)$ , and [F1] preserves their independence. Thus $Z = (Z_{1}, \dots, Z_{n}) \sim N_{n} (0, I_{n})$ by [F4].

2.1step 1.1algebra

Define $\overset{ˉ}{Z} = n^{- 1} \sum_{i = 1}^{n} Z_{i}$ , $u = n^{- 1 / 2} (1, \dots, 1)^{T}$ , and $P = u u^{T}$ . Since $u^{T} u = 1$ , $P$ is a rank-one orthogonal projection. We have $u^{T} Z = \sqrt{n} \overset{ˉ}{Z}$ and $X - \overset{ˉ}{X} (1, \dots, 1)^{T} = σ (I_{n} - P) Z$ . Therefore $\overset{ˉ}{X} = μ + σ u^{T} Z / \sqrt{n}$ and $S^{2} = σ^{2} ∥ (I_{n} - P) Z ∥^{2} / (n - 1)$ .

3.1A2F1F2F3F4algebrastep 2.1

By [F3], $P Z$ and $(I_{n} - P) Z$ are independent and $Q : = ∥ (I_{n} - P) Z ∥^{2} \sim χ_{n - 1}^{2}$ . The continuous linear map $z \mapsto u^{T} z$ is Borel by [A2] and [F2], and $u^{T} Z = u^{T} P Z$ ; the continuous squared-norm map on the complementary vector is likewise Borel. Thus $G : = u^{T} Z$ and $Q$ are measurable functions of the independent vectors in [F3], so they are independent by [F1]. By [F4], $G \sim N (0, 1)$ .

4.1step 2.1step 3.1F1F5algebra

The formulas in step 2.1 express $\overset{ˉ}{X}$ as an affine function of $G$ and $S^{2}$ as $σ^{2} Q / (n - 1)$ . Hence $\overset{ˉ}{X}$ and $S^{2}$ are independent, $(n - 1) S^{2} / σ^{2} = Q \sim χ_{n - 1}^{2}$ , and $S > 0$ almost surely by [F5].

5.1step 2.1step 3.1step 4.1F5algebra

The set ${S > 0}$ is Borel and the displayed quotient is continuous there; assigning $0$ on ${S = 0}$ therefore makes $\tilde{T}$ measurable. Since $S = 0$ exactly when $Q = 0$ , step 2.1 gives $\tilde{T} = G / \sqrt{Q / (n - 1)}$ on ${Q > 0}$ and both versions are $0$ on ${Q = 0}$ . The variables $G$ and $Q$ are independent with laws $N (0, 1)$ and $χ_{n - 1}^{2}$ , so [F5] gives $\tilde{T} \sim t_{n - 1}$ .

6.1F5step 4.1step 5.1algebra∎

Let $q = q_{n - 1} (1 - α / 2)$ . By [F5], the $t_{n - 1}$ CDF is continuous and symmetric, so $F_{t_{n - 1}} (0) = 1 / 2 < 1 - α / 2$ and strict increase gives $q > 0$ ; symmetry then gives $F_{t_{n - 1}} (- q) = α / 2$ . Step 5.1 therefore gives $P (- q \leq \tilde{T} \leq q) = 1 - α$ . On the full-probability event ${S > 0}$ from step 4.1, this event is exactly ${μ lies in the displayed interval}$ by multiplying by $S / \sqrt{n}$ and rearranging. The events agree almost surely, so the interval has exact coverage $1 - α$ .

Depends on

Used by

Dependency tree · two levels

61 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

Dmitry Panchenko, MIT 18.443 Statistics for Applications, Fall 2003, Lecture 17 (standard reference, not scraped)
Aditya Guntuboyina, UC Berkeley Stat 201A Fall 2019, Lecture Notes, §5.5 (standard reference, not scraped)
Joshua M. Tebbs, STAT 512 Lecture Notes, Chapter 8, §8.7.1 (standard reference, not scraped)