LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-21

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 square of the one-dimensional Gaussian integral is the plane Gaussian integral

Statement

Let $I = \int_{- \infty}^{\infty} e^{- x^{2}} d x$ . Then

$I^{2} = \int_{R^{2}} e^{- (x^{2} + y^{2})} d (x, y) .$

The plane integral is the nonnegative improper multiple integral.

Facts & Assumptions

Given: The finite positive number $I$ and the nonnegative plane Gaussian.

[L1]

For continuous $a$ and $b$ on rectangles, $\int_{A \times B} a (x) b (y) = (\int_{A} a) (\int_{B} b)$ (The integral of a product function on a product rectangle is the product of the two integrals).

[L2]

Every compact Jordan exhaustion computes the nonnegative improper integral, independently of the exhaustion (Every Jordan exhaustion computes a nonnegative improper multiple integral).

[L3]

The integral $I = \int_{- \infty}^{\infty} e^{- x^{2}} d x$ exists as a finite positive real number (The improper integral of $e^{- x^{2}}$ over $R$ is finite and positive).

[L4]

The exponential satisfies $\exp (u + v) = \exp (u) \exp (v)$ (The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ ).

Proof

technique · direct

1.1

For $R > 0$ , [L4] gives $e^{- (x^{2} + y^{2})} = e^{- x^{2}} e^{- y^{2}}$ , so [L1] yields $\int_{[- R, R]^{2}} e^{- (x^{2} + y^{2})} d (x, y) = {(\int_{- R}^{R} e^{- x^{2}} d x)}^{2}$ .

L1L4

2.1

Put $R = j + 1$ . The squares form a compact Jordan exhaustion of $R^{2}$ , so [L2] makes their plane integrals tend to the nonnegative improper plane integral; [L3] makes each one-dimensional factor tend to $I$ .

step 1.1L2L3

3.1

Passing to the limit in the product identity of step 1.1 gives the plane integral equal to $I^{2}$ .

step 2.1algebra∎

Depends on

Used by

The Gaussian integral ∫_-∞^∞e^-x² dx=√π Theorem

Dependency tree · two levels

28 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

M. E. Taylor, Introduction to Analysis in Several Variables, formulas (3.1.71)–(3.1.75) (standard reference, not scraped)