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 is positive and Borel measurable on , with Lebesgue integral one.
Facts & Assumptions
The power-series, product-limit, IVP, functional-equation, and Picard definitions agree: The following descriptions give the same function : the power series ; the product limit ; the normalized solution of ; the normalized continuous multiplicative function; and the compact-uniform limit of the Picard iterates.
The exponential function is smooth and : The real exponential function is , and for every , In particular .
Continuous functions on Euclidean spaces are Borel measurable: Assume the Axiom of Countable Choice. Let . Every continuous map is Borel measurable in the sense of def-borel-and-lebesgue-measurable-function-on-rn.
Square roots exist: a unique with ; the positives are : Let be a complete ordered field (def-complete-ordered-field). Then every with has a unique with and ; we write . Consequently the positive elements of are exactly the nonzero squares: if and only if for some .
Substitution: if is differentiable on with integrable and is continuous on an interval containing , then : Let be reals and let be differentiable at every point of as a function on (def-derivative), with integrable on (def-darboux-integral). Let be order-convex with at least two elements (def-interval) with , and let be continuous on (def-continuity-real).
Then is integrable on and
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: may lie below , and may return to the same value many times. The proof runs through a primitive of and the chain rule, and no inverse function is ever formed.
Continuity of is a hypothesis and cannot be weakened to integrability. With merely integrable the composite 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.
A continuous function on is Riemann integrable, by Heine-Cantor and Riemann's criterion: Let be reals and let be continuous on (def-continuity-real). Then is bounded (def-bounded-set) and Riemann integrable on (def-darboux-integral).
The proof gives more than integrability: it gives a partition that works. For every real the uniform partition into parts already satisfies , as soon as is large enough that is below the that uniform continuity supplies for . Uniform continuity is exactly what makes one serve all subintervals at once, and it is the only place where the compactness of is used.
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 and let be bounded and Riemann integrable. Then is Lebesgue measurable on and is integrable there, and its Lebesgue integral equals its Riemann integral:
This is the point at which the completeness of Lebesgue measure is used essentially: the proof obtains a Borel function equal to almost everywhere, and measurability of itself is then a completeness statement.
Monotone convergence for the integral: Let be measurable and suppose for every . Then
Monotonicity and nonnegative homogeneity of the nonnegative integral: Let be measurable and let .
- If , then .
- .
Proof
Given: The objects, hypotheses and definitions in the statement. Its conclusions are to be established below.
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.
For integer , F5 with and continuous f(t)=exp(-t^2) gives . 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.
The nonnegative functions increase to . By F8, its Lebesgue integral is the limit of the compact integrals in step 2.1. F9 identifies the right-hand improper limit as ; 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.
Depends on
- The Gaussian integral $\int_{-\infty}^{\infty}e^{-x^2}\,dx=\sqrt{\pi}$
- Substitution: if $\varphi$ is differentiable on $[c,d]$ with $\varphi'$ integrable and $f$ is continuous on an interval containing $\varphi([c,d])$, then $\int_{\varphi(c)}^{\varphi(d)} f = \int_c^d (f\circ\varphi)\,\varphi'$
- A continuous function on $[a,b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion
- A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral
- Monotone convergence for the integral
- The power-series, product-limit, IVP, functional-equation, and Picard definitions agree
- The exponential function is smooth and $(\exp)'=\exp$
- Continuous functions on Euclidean spaces are Borel measurable
- Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$; the positives are $\{x^2 : x \neq 0\}$
- Monotonicity and nonnegative homogeneity of the nonnegative integral
- The Axiom of Choice
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
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
- Durrett, Probability: Theory and Examples, Example 1.6.11, p.34; local normalization from the earlier published Gaussian integral (standard reference, not scraped)