LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

A normal variable has finite fourth moment

Statement

Assume AC and let $G \sim N (0, σ^{2})$ for $σ \geq 0$ . Then $E [G^{2}] = σ^{2}$ and $E [G^{4}] = 3 σ^{4}$ ; in particular the fourth moment is finite. For independent centered normal coordinates $G_{j} \sim N (0, σ_{j}^{2})$ , every finite linear combination of the variables $G_{j}^{2}$ has finite second moment.

Facts & Assumptions

Given: AC and a scalar centered normal variable with variance $σ^{2} \geq 0$ .

[A1]

The Axiom of Choice and Standard normal and normal laws: the standard normal law is defined under AC and has density $ϕ (x) = (2 π)^{- 1 / 2} e^{- x^{2} / 2}$ .

[F1]

The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ and Change of variable in an improper integral: $\int_{R} e^{- x^{2} / 2} d x = \sqrt{2 π}$ .

[F2]

If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ : on finite intervals, $\int u v^{'} = u v ∣_{a}^{b} - \int u^{'} v$ under its stated integrability hypotheses.

[F3]

The exponential dominates every fixed nonnegative integer power at $+ \infty$ : a fixed polynomial times $e^{- x^{2} / 2}$ tends to zero as $∣ x ∣ \to \infty$ and is integrable after comparison with a weaker Gaussian tail.

[F4]

The exponential function is smooth and $(\exp)^{'} = \exp$ gives $\exp^{'} = \exp$ ; The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ gives $(e^{u (x)})^{'} = e^{u (x)} u^{'} (x)$ for differentiable $u$ on an open interval. The product and scalar rules in Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ give $(x^{2})^{'} = 2 x$ , so $u (x) = - x^{2} / 2$ has derivative $- x$ .

[F5]

Expectations factor over finite products of independent random variables: for independent variables, integrable Borel functions of the individual variables have integrable product and factorized product expectation.

Proof

1.1F1F2F3given

Let $I_{k} : = \int_{R} x^{2 k} e^{- x^{2} / 2} d x$ for $k = 0, 1, 2$ . These integrals are finite: outside a bounded interval, $∣ x ∣^{2 k} e^{- x^{2} / 4}$ is bounded by [F3], while $e^{- x^{2} / 4}$ is integrable by [F1] after scaling. Thus integration by parts on $[- R, R]$ is valid, and its polynomial-exponential boundary terms vanish as $R \to \infty$ by [F3].

2.1A1F1F2F3F4step 1.1algebra

Since $u (x) = - x^{2} / 2$ is differentiable on $R$ and the exponential is differentiable at every $u (x)$ , the chain rule in [F4] gives $(e^{- x^{2} / 2})^{'} = - x e^{- x^{2} / 2}$ . All these functions and derivatives are continuous on $[- R, R]$ , so the hypotheses of [F2] hold. Integration by parts gives $\int_{- R}^{R} x^{2} e^{- x^{2} / 2} d x = [- x e^{- x^{2} / 2}]_{- R}^{R} + \int_{- R}^{R} e^{- x^{2} / 2} d x$ and $\int_{- R}^{R} x^{4} e^{- x^{2} / 2} d x = [- x^{3} e^{- x^{2} / 2}]_{- R}^{R} + 3 \int_{- R}^{R} x^{2} e^{- x^{2} / 2} d x$ . Letting $R \to \infty$ , [F3] makes the boundary terms vanish and [F1] gives $I_{1} = I_{0} = \sqrt{2 π}$ and $I_{2} = 3 I_{1} = 3 \sqrt{2 π}$ ; integration against the standard-normal density gives $E [G_{0}^{2}] = 1$ and $E [G_{0}^{4}] = 3$ .

3.1A1F5step 2.1givencasesalgebra∎

If $σ > 0$ , the definition of $N (0, σ^{2})$ is the law of $σ G_{0}$ , so $E [G^{2}] = σ^{2} E [G_{0}^{2}] = σ^{2}$ and $E [G^{4}] = σ^{4} E [G_{0}^{4}] = 3 σ^{4}$ . If $σ = 0$ , $G = 0$ almost surely and both formulas hold. For distinct indices $i \neq j$ , the squared coordinates are integrable by these second-moment formulas, so [F5] gives $E [G_{i}^{2} G_{j}^{2}] = σ_{i}^{2} σ_{j}^{2} < \infty$ . For $i = j$ , the fourth-moment formula instead gives $E [G_{i}^{4}] = 3 σ_{i}^{4} < \infty$ . Thus every term in the square of a finite linear combination of the $G_{j}^{2}$ is integrable, proving that combination has finite second moment; the empty combination is zero.

Depends on

Used by

Dependency tree · two levels

65 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

Yury Polyanskiy and Yihong Wu, Information Theory: From Coding to Learning, Chapter 2 §2.3 (standard reference, not scraped)
David J. C. MacKay, Information Theory, Inference, and Learning Algorithms, Chapter 12 §12.3 (standard reference, not scraped)