ExampleConstruction: AI-generatedVerification: 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.

Exact unknown-variance normal t interval

Example

Assume AC and let $n \geq 2$ . For each fixed variance $λ = σ^{2} > 0$ , let ${\tilde{P}}_{μ, λ} = N (μ, λ)^{\otimes n}$ be the full product law on $R^{n}$ , with mean parameter $μ \in R$ and independent coordinates. Use the common sample space $D_{n} : = {x \in R^{n} : s (x) > 0}$ , where $\overset{ˉ}{x} = n^{- 1} \sum_{i} x_{i}$ and $s (x) : = \sqrt{(n - 1)^{- 1} \sum_{i} (x_{i} - \overset{ˉ}{x})^{2}}$ is the nonnegative square root, with the trace Borel sigma-algebra; write $P_{μ, λ}$ for the restriction of ${\tilde{P}}_{μ, λ}$ to this sample space. Let $ν = n - 1$ , and write $t_{ν, u}$ for the unique $u$ -quantile of the $t_{ν}$ law. For $0 < α < 1$ , the interval $I (X) = [\overset{ˉ}{X} - t_{ν, 1 - α / 2} \frac{S}{\sqrt{n}}, \overset{ˉ}{X} + t_{ν, 1 - α / 2} \frac{S}{\sqrt{n}}]$ has exact coverage $P_{μ, λ} {μ \in I (X)} = 1 - α$ , for every $μ \in R$ and every fixed $λ > 0$ . The same formula works for all unknown variances.

Facts & Assumptions

Given: AC, $n \geq 2$ , $0 < α < 1$ , and for each $λ > 0$ the iid normal experiment indexed by $μ \in R$ .

[A1]

The Axiom of Choice: AC is the axiom assumed by the normal-law construction and the two Gaussian suppliers used here.

[F1]

Normal sample mean and residual are independent, giving the exact t pivot: for an iid $N (μ, σ^{2})$ sample with $n \geq 2$ , $S > 0$ almost surely and $(\overset{ˉ}{X} - μ) / (S / \sqrt{n})$ has the $t_{n - 1}$ law.

[F2]

Student t and Fisher F CDFs are continuous and strictly increasing on their supports: for $ν \geq 1$ , the $t_{ν}$ CDF is continuous, strictly increasing, symmetric about zero, and has limits zero and one, so each $u \in (0, 1)$ has a unique quantile.

[F3]

Confidence sets and coverage: a confidence-set procedure has measurable membership sections, and its coverage at a parameter is the probability of the corresponding section.

[F4]

Pivotal quantities: a family of measurable maps, one for each parameter, is a pivot when every map has the same pushforward probability law.

[F5]

Coverage from pivot inversion and exact calibration: inversion of a pivot acceptance set of probability $1 - α$ gives exact coverage $1 - α$ at every parameter.

[F6]

The Borel sigma-algebra of a topological space: the Borel sigma-algebra is generated by the open sets; on $D_{n}$ we use the trace of the Borel sigma-algebra of $R^{n}$ .

[F7]

Statistical experiments: an experiment consists of a measurable sample space, a parameter set, and one probability law on that space for each parameter.

Verification

1.1givenA1F1F6F7

For all $x, y \in R^{n}$ , $∣ \overset{ˉ}{x} - \overset{ˉ}{y} ∣ \leq \max_{i} ∣ x_{i} - y_{i} ∣ \leq ∥ x - y ∥_{2}$ . The residual map $r (x) = x - \overset{ˉ}{x} 1$ is linear and orthogonal to $1$ , so Pythagoras gives $∥ r (x - y) ∥_{2} \leq ∥ x - y ∥_{2}$ ; the reverse triangle inequality then gives $∣ s (x) - s (y) ∣ \leq ∥ x - y ∥_{2} / \sqrt{n - 1}$ . Hence $s$ is continuous, $D_{n} = {x : s (x) > 0}$ is open, and its trace Borel sets form a sigma-algebra by [F6]. By [F1], every full law ${\tilde{P}}_{μ, λ}$ gives $D_{n}$ probability one, so its restriction $P_{μ, λ}$ remains a probability measure; [F7] therefore gives the stated experiment for each fixed $λ > 0$ .

1.2givenF2algebra

Put $c = t_{ν, 1 - α / 2}$ , which exists uniquely by [F2]. Symmetry and continuity give $F_{t_{ν}} (0) = 1 / 2$ ; strict increase and $1 - α / 2 > 1 / 2$ imply $c > 0$ . Since $F_{t_{ν}} (c) = 1 - α / 2$ , symmetry gives $F_{t_{ν}} (- c) = α / 2$ ; continuity means neither endpoint is an atom, so $P (- c \leq T_{ν} \leq c) = 1 - α$ .

1.3givenA1F1F4F6

For each candidate mean $η \in R$ , define $q_{η} (x) = (\overset{ˉ}{x} - η) / (s (x) / \sqrt{n})$ on $D_{n}$ . Its denominator is positive there, so it is continuous and hence measurable on the subspace $D_{n}$ by the open-set definition of its trace Borel sigma-algebra [F6]. For every Borel $B \subseteq R$ , the restricted probability satisfies $P_{η, λ} {q_{η} \in B} = {\tilde{P}}_{η, λ} {x \in D_{n} : q_{η} (x) \in B}$ , and [F1] gives this value as the common $t_{ν}$ probability because the full law assigns probability one to $D_{n}$ . Thus $(q_{η})_{η \in R}$ is a pivot by [F4].

2.1givenF3F4F5step 1.2algebra∎

Inverting $B = [- c, c]$ gives ${η : q_{η} (x) \in B} = [\overset{ˉ}{x} - c s (x) / \sqrt{n}, \overset{ˉ}{x} + c s (x) / \sqrt{n}] = I (x)$ by solving the two inequalities, and each membership section is measurable because $q_{η}$ is measurable. Step 1.2 gives the pivot mass $ν (B) = 1 - α$ ; the pivot-inversion theorem [F5] and confidence-set definition [F3] therefore give exact coverage $1 - α$ for every mean and every fixed variance.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 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

Anna Mikusheva, MIT 14.381, Lecture 11: Confidence Sets, §2, PDF p. 3 (standard reference, not scraped)
Karl B. Gregory, USC STAT 713, Lecture 14: Confidence Intervals and Sets, slides 8 and 12, PDF pp. 10 and 20 (standard reference, not scraped)