LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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 mean of a finite independent normal sample is normal

Statement

Assume AC. Let $n \geq 1$ , and let $X_{1}, \dots, X_{n}$ be mutually independent real random variables on one probability space, each with law $N (μ, σ^{2})$ for a fixed $μ \in R$ and $σ \geq 0$ . Then ${\overset{ˉ}{X}}_{n} = n^{- 1} \sum_{i = 1}^{n} X_{i}$ has law $N (μ, σ^{2} / n)$ . If $σ > 0$ , then for every $μ_{0} \in R$ , $\frac{\sqrt{n} ({\overset{ˉ}{X}}_{n} - μ_{0})}{σ} \sim N ⁣ (\frac{\sqrt{n} (μ - μ_{0})}{σ}, 1) .$

Facts & Assumptions

Given: AC, a positive integer $n$ , mutually independent $X_{1}, \dots, X_{n}$ , and their common normal law $N (μ, σ^{2})$ with $σ \geq 0$ .

[A1]

The standard normal and its affine normal laws are defined under AC. The Axiom of Choice Standard normal and normal laws

[F0]

The characteristic function of a real random variable $X$ is $φ_{X} (t) = E [e^{i t X}]$ for real $t$ . Characteristic function of a real random variable

[F1]

If $X \sim N (m, s^{2})$ , then its characteristic function is $φ_{X} (t) = \exp (i m t - s^{2} t^{2} / 2)$ . Characteristic function of a normal law

[F2]

For a finite mutually independent family, the characteristic function of the sum is the product of the individual characteristic functions, and $φ_{a X + b} (t) = e^{i t b} φ_{X} (a t)$ . Independent random elements Characteristic functions under affine maps and independent sums

[F3]

Borel probability laws on $R$ with the same characteristic function are equal. Uniqueness of a law from its characteristic function

[F4]

The complex exponential satisfies $e^{z + w} = e^{z} e^{w}$ , so finite repeated products combine by adding exponents. $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential

Proof

1.1A1F0F1F2F4algebra

By [F0] and [F2], for every $t \in R$ , $φ_{{\overset{ˉ}{X}}_{n}} (t) = φ_{\sum_{i} X_{i}} (t / n) = \prod_{i = 1}^{n} φ_{X_{i}} (t / n) = {[\exp ⁣ (i μ t / n - σ^{2} t^{2} / (2 n^{2}))]}^{n} = \exp ⁣ (i μ t - σ^{2} t^{2} / (2 n))$ , where [F1] supplies each factor and [F4] combines the $n$ exponents.

2.1A1F0F1F2F3step 1.1algebra∎

By [F1], the last expression is the characteristic function of $N (μ, σ^{2} / n)$ . Uniqueness [F3] proves ${\overset{ˉ}{X}}_{n} \sim N (μ, σ^{2} / n)$ . When $σ > 0$ , the affine identity in [F2] applied to $\sqrt{n} ({\overset{ˉ}{X}}_{n} - μ_{0}) / σ$ gives the stated shifted $N (\cdot, 1)$ law. The same calculation covers $σ = 0$ , where both laws are point masses at their respective means.

Depends on

Used by

Dependency tree · two levels

47 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

Rick Durrett, Probability: Theory and Examples, 5th ed., §3.3.1–§3.3.2, Example 3.3.5 and Corollary 3.3.13, printed pp. 125–130 (standard reference, not scraped)