ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 2026-09-13

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.

CLT for sums of uniform random variables

Example

Assume AC. If $(U_{k})$ are iid with density $1_{[0, 1]}$ , then $\sqrt{12 / n} (\sum_{k = 1}^{n} U_{k} - n / 2) \Rightarrow N (0, 1) .$

Facts & Assumptions

[F1]

The indicator density of [0,1] defines a measure. The indefinite integral of a nonnegative measurable function is a measure.

[F2]

For nonnegative measurable functions, integration under this law equals integration of the function times its density. Integrating against a density agrees with integrating the product.

[F3]

Continuous polynomial derivatives integrate to primitive differences. The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ .

[F4]

The derivatives of the relevant integer powers have the usual coefficients. For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term.

[F5]

The compact Riemann and Lebesgue integrals agree under countable choice. A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral.

[F6]

Under DC and countable choice a given law has countably many independent copies. Countably many independent copies of a prescribed law exist.

[F7]

AC implies the two choice principles required for independent copies. AC supplies countable selections and prescribed serial paths.

[F8]

The iid CLT applies to finite positive variance. Lindeberg-Levy iid central limit theorem.

[F9]

Continuous compact-interval powers are Riemann integrable. A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion.

[F10]

A real integral is the integral of the positive part minus the integral of the negative part. Integrable real and complex functions, and their integrals.

Verification

Given: Assume AC. If $(U_{k})$ are iid with density $1_{[0, 1]}$ , then $\sqrt{12 / n} (\sum_{k = 1}^{n} U_{k} - n / 2) \Rightarrow N (0, 1) .$

1.1

The nonnegative Borel density $1_{[0, 1]}$ defines a measure by [F1]. On [0,1] the primitives x, $x^{2} / 2$ and $x^{3} / 3$ have derivatives 1,x and $x^{2}$ by [F4]. Those derivatives are continuous and integrable by [F9], so [F3] and [F5] give integrals 1,1/2 and 1/3 respectively. Thus the measure is a probability. Apply [F2] separately to the globally nonnegative functions $x^{+} = \max {x, 0}$ and $x^{-} = \max {- x, 0}$ . Their products with the density are respectively $x 1_{[0, 1]}$ and zero, so [F10] gives $E U = 1 / 2 - 0 = 1 / 2$ . Applying [F2] to the nonnegative function $x^{2}$ gives $E U^{2} = 1 / 3$ , hence $Var (U) = 1 / 3 - 1 / 4 = 1 / 12$ . The density-supported integrands are bounded, so no tail or improper integral is involved.

F1F2F3F4F5F9F10

2.1

If copies need realization, [F7] lets AC supply the DC and countable choice in [F6]; the resulting coordinate variables have exactly this density law and are iid. For given iid U_k the same moment computation applies. [F8] gives $(\sum_{k} U_{k} - n / 2) / \sqrt{n / 12} \Rightarrow N (0, 1)$ , and $1 / \sqrt{n / 12} = \sqrt{12 / n}$ proves the displayed form. The variance is strictly positive and n>=1, so the normalization is defined. AC is used in the integral bridge, copy construction when needed, and CLT supplier.

step 1.1F6F7F8∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

81 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

Durrett, Probability: Theory and Examples, Section 3.4.1 (standard reference, not scraped)
Aldous and Chewi, Probability Theory notes, Theorem 5.2 (standard reference, not scraped)