Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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 standard normal density has total mass one

Statement

Assume AC. The function ϕ(x)=ex2/2/2π is positive and Borel measurable on R, with Lebesgue integral one.

Facts & Assumptions

[F1]

The power-series, product-limit, IVP, functional-equation, and Picard definitions agree: The following descriptions give the same function R(0,): the power series xn/n!; the product limit limn(1+x/n)n; the normalized solution of y=y, y(0)=1; the normalized continuous multiplicative function; and the compact-uniform limit of the Picard iterates.

[F2]

The exponential function is smooth and (exp)=exp: The real exponential function is C, and for every mN, exp(m)=exp. In particular (exp)=exp.

[F3]

Continuous functions on Euclidean spaces are Borel measurable: Assume the Axiom of Countable Choice. Let n,m1. Every continuous map f:RnRm is Borel measurable in the sense of def-borel-and-lebesgue-measurable-function-on-rn.

[F4]

Square roots exist: a unique a0 with (a)2=a; the positives are {x2:x0}: Let F be a complete ordered field (def-complete-ordered-field). Then every aF with a0 has a unique sF with s0 and s2=a; we write s=a. Consequently the positive elements of F are exactly the nonzero squares: x>0 if and only if x=y2 for some y0.

[F5]

Substitution: if φ is differentiable on [c,d] with φ integrable and f is continuous on an interval containing φ([c,d]), then φ(c)φ(d)f=cd(fφ)φ: Let c<d be reals and let φ:[c,d]R be differentiable at every point of [c,d] as a function on [c,d] (def-derivative), with φ integrable on [c,d] (def-darboux-integral). Let JR be order-convex with at least two elements (def-interval) with φ[[c,d]]J, and let f:JR be continuous on J (def-continuity-real).

Then (fφ)φ is integrable on [c,d] and

φ(c)φ(d)f  =  cd(fφ)φ,

the left-hand integral being the oriented one of def-oriented-integral.

Neither injectivity nor monotonicity of φ is assumed, and that is exactly why the left-hand side is written with oriented limits: φ(d) may lie below φ(c), and φ may return to the same value many times. The proof runs through a primitive of f and the chain rule, and no inverse function is ever formed.

Continuity of f is a hypothesis and cannot be weakened to integrability. With f merely integrable the composite fφ need not be integrable at all, so the right-hand side need not exist; that is the false statement that weakens it on the companion page.

[F6]

A continuous function on [a,b] is Riemann integrable, by Heine-Cantor and Riemann's criterion: Let a<b be reals and let f:[a,b]R be continuous on [a,b] (def-continuity-real). Then f is bounded (def-bounded-set) and Riemann integrable on [a,b] (def-darboux-integral).

The proof gives more than integrability: it gives a partition that works. For every real ε>0 the uniform partition into N parts already satisfies U(f,P)L(f,P)<ε, as soon as N is large enough that (ba)/N is below the δ that uniform continuity supplies for ε/(2(ba)). Uniform continuity is exactly what makes one δ serve all N subintervals at once, and it is the only place where the compactness of [a,b] is used.

[F7]

A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral: Assume the Axiom of Countable Choice. Let a<b and let f:[a,b]R be bounded and Riemann integrable. Then f is Lebesgue measurable on [a,b] and is integrable there, and its Lebesgue integral equals its Riemann integral: [a,b]fdλ1=abf(x)dx.

This is the point at which the completeness of Lebesgue measure is used essentially: the proof obtains a Borel function equal to f almost everywhere, and measurability of f itself is then a completeness statement.

[F8]

Monotone convergence for the integral: Let 0f1f2 be measurable and suppose fn(x)f(x) for every x. Then fndμfdμ.

[F9]

The Gaussian integral ex2dx=π: ex2dx=π.

[F10]

Monotonicity and nonnegative homogeneity of the nonnegative integral: Let f,g:X[0,+] be measurable and let c0.

  1. If fg, then fdμgdμ.
  2. cfdμ=cfdμ.

Proof

Given: The objects, hypotheses and definitions in the statement. Its conclusions are to be established below.

1.1

F1 gives positivity of the exponential, and F2 gives continuity. Thus ϕ is positive and continuous. AC restricts to a choice function on every countable nonempty family, giving CC; F3 therefore applies to ϕ. F4 makes its positive denominator well defined.

F1F2F3F4
2.1

For integer n1, F5 with φ(x)=x/2 and continuous f(t)=exp(-t^2) gives nnex2/2dx=2n/2n/2et2dt. The derivative is the constant 1/sqrt2, hence integrable. Both integrands are continuous on the compact intervals, so F6 gives bounded Riemann integrability. F7 identifies the left side with its Lebesgue integral, under the CC in step 1.1.

F5F6F7step 1.1
3.1

The nonnegative functions ex2/21[n,n] increase to ex2/2. By F8, its Lebesgue integral is the limit of the compact integrals in step 2.1. F9 identifies the right-hand improper limit as 2π=2π; the equality follows because both sides are positive with square 2pi, by square-root uniqueness. F10 now divides by sqrt(2pi) to give integral ϕ=1.

F8F9F10step 2.1

Depends on

Used by

Dependency tree · two levels

84 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