LemmaStatement: 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.

Box–Muller has a product Gaussian density and Rayleigh second moment

Statement

Assume Countable Choice. Let $(U, V)$ have product Lebesgue probability law on $(0, 1)^{2}$ , and set $R = \sqrt{- 2 \log U}, Θ = 2 π V, Z = (R \cos Θ, R \sin Θ) .$ Then $Z$ has the Borel density $g (x, y) = \frac{1}{2 π} e^{- (x^{2} + y^{2}) / 2} = ϕ (x) ϕ (y), ϕ (t) = \frac{e^{- t^{2} / 2}}{\sqrt{2 π}} .$ In particular, its coordinates are independent with density $ϕ$ . Also $P (R > r) = e^{- r^{2} / 2}$ for $r \geq 0$ and $E R^{2} = 2$ .

Facts & Assumptions

Given: Countable Choice and the joint-uniform pair and transform in the Statement.

[F1]

For a $C^{1}$ diffeomorphism between open Euclidean sets, nonnegative Borel change of variables is valid under Countable Choice. Borel change of variables from the compact-support formula and Radon uniqueness

[F2]

A coordinate hyperplane has two-dimensional Lebesgue measure zero under Countable Choice. A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in $R^{n}$

[F3]

Tonelli's theorem factors nonnegative integrals on sigma-finite product spaces and allows order exchange. Tonelli's theorem for nonnegative measurable functions on a sigma-finite product

[F4]

Independence means independence of the generated sigma-algebras; factorization of probabilities on every finite Borel rectangle is an equivalent criterion. Independent random elements, Independent random elements are characterized by finite rectangle probabilities

[F5]

A probability measure has total mass one, and its pushforward law is again a probability measure. Probability measures and probability spaces

[F6]

Continuous maps pull Borel functions back to Borel functions. A continuous map has Borel preimages of Borel sets

[F7]

The exponential derivative, chain rule, logarithm identity, and square-root law justify the displayed transform derivatives and radial inverse; $π$ is the fixed positive constant of the trigonometric coordinate. The real exponential function and the number $e$ by a power series, The exponential function is strictly increasing, The exponential function is smooth and $(\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)$ , Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Pi as twice the smallest positive zero of cosine

[F8]

The logarithm is the inverse of the exponential: $\exp (\log u) = u$ for $u > 0$ and $\log (\exp t) = t$ for real $t$ . Also $\log^{'} (u) = 1 / u$ ; differentiating the inverse of $s \mapsto s^{2}$ on $(0, \infty)$ gives $(\sqrt{t})^{'} = 1 / (2 \sqrt{t})$ . Exponentials satisfy $\exp (s + t) = \exp (s) \exp (t)$ . The natural logarithm as the inverse of the exponential function, The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, Derivative of an inverse: if $f$ is continuous and injective on a nondegenerate interval $I$ and differentiable at $c \in I$ with $f^{'} (c) \neq 0$ , then the inverse $g$ is differentiable at $f (c)$ with $g^{'} (f (c)) = 1 / f^{'} (c)$ ; and if $f^{'} (c) = 0$ then $g$ is not differentiable at $f (c)$ , The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$

[F9]

The map $θ \mapsto (\cos θ, \sin θ)$ bijects $[0, 2 π)$ onto the unit circle, and its component derivatives are $- \sin θ$ and $\cos θ$ . A $C^{1}$ map between open Euclidean sets with invertible derivative has a local $C^{1}$ inverse with the inverse derivative. $t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the real unit circle, The derivatives of sine and cosine are cosine and minus sine, The Euclidean inverse function theorem

[A1]

Countable Choice is the only choice assumption used by the change-of-variables and null-axis suppliers; no use is made of full Choice. The Axiom of Countable Choice ( ${A C}_{ω}$ )

Proof

Given: As in the Statement. Let $D = R^{2} ∖ {(x, 0) : x \geq 0}$ , an open slit plane. The map $G (x, y) = (e^{- (x^{2} + y^{2}) / 2}, \frac{\arg_{(0, 2 π)} (x + i y)}{2 π})$ will be shown to be the inverse of the displayed Box–Muller map $T$ from $(0, 1)^{2}$ onto $D$ .

1.1givenF7F8F9algebra

By [F7]–[F8], $r (u) = \sqrt{- 2 \log u}$ is positive on $(0, 1)$ , with inverse $u = e^{- r^{2} / 2}$ for $r > 0$ . By [F9], the angles $2 π v$ for $0 < v < 1$ parametrize the unit circle with $(1, 0)$ removed exactly once. Thus $T$ is bijective onto $D$ , with inverse $G$ . The scalar derivatives give $r^{'} (u) = - 1 / (u r (u))$ , so $T$ is $C^{1}$ and $\det D T (u, v) = 2 π r (u) r^{'} (u) = - 2 π / u \neq 0$ . The local inverse theorem [F9], together with global bijectivity, makes $G$ a $C^{1}$ inverse on $D$ , with $∣ \det D G (x, y) ∣ = e^{- (x^{2} + y^{2}) / 2} / (2 π)$ .

2.1givenF1F2F6A1step 1.1

For every nonnegative Borel $h$ on $D$ , [F6] makes $h \circ T$ Borel. Apply [F1] to $G : D \to (0, 1)^{2}$ with integrand $h \circ T$ on its target. Since $(U, V)$ has product Lebesgue law, this gives $E [h (Z)] = \int_{D} h (x, y) g (x, y) d x d y$ . The omitted nonnegative $x$ -axis is Borel and null by [F2], and $Z$ always lies in $D$ , so $g$ is the density on all of $R^{2}$ .

3.1F3F4F5F8step 2.1algebra

By [F5], the pushforward law has total mass one, so its density integrates to $1$ . By [F3] and the exponential addition law [F8], writing $A = \int_{R} e^{- t^{2} / 2} d t \in (0, \infty]$ , we have $1 = (2 π)^{- 1} A^{2}$ . Positivity of the integrand gives $A > 0$ , and the equality forces $A < \infty$ and $A = \sqrt{2 π}$ . Therefore $g (x, y) = ϕ (x) ϕ (y)$ with each factor integrating to $1$ . For arbitrary Borel sets $A, B \subseteq R$ , [F3] applied to $1_{A} (x) 1_{B} (y) ϕ (x) ϕ (y)$ gives $P (Z_{1} \in A, Z_{2} \in B) = (\int_{A} ϕ) (\int_{B} ϕ)$ . Taking $B = R$ or $A = R$ identifies the marginal probabilities. Thus the Borel-rectangle factorization criterion [F4] proves independence, with the stated marginal densities.

4.1givenF3F7F8algebra∎

For $r \geq 0$ , monotonicity and the inverse identities [F7]–[F8] give ${R > r} = {U < e^{- r^{2} / 2}}$ ; uniformity gives probability $e^{- r^{2} / 2}$ , also at $r = 0$ . Pointwise, $R^{2} = \int_{0}^{\infty} 2 t 1_{{t < R}} d t$ . By [F3], $E R^{2} = \int_{0}^{\infty} 2 t e^{- t^{2} / 2} d t = 2$ , using the substitution $s = t^{2} / 2$ .

Depends on

Used by

Dependency tree · two levels

125 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

Luc Devroye, Non-Uniform Random Variate Generation, Chapter V §4.4, Box–Muller method (standard reference, not scraped)
E. M. Raz, Lecture Notes in Probability, Chapter 5, Exercise 5.2 (standard reference, not scraped)