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.
Characteristic function of a normal law
Statement
Assume AC. If has law with , then for every real . Moreover and , including .
Facts & Assumptions
Under AC the normal laws are the affine images of the standard density law. Standard normal and normal laws.
The positive Borel density g has total integral one. The standard normal density has total mass one.
The real exponential is smooth with derivative itself. The exponential function is smooth and .
The chain rule differentiates the quadratic composition. The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with .
The product and linearity rules apply to real components. Sums, scalar multiples, products and quotients: , , , and when .
Continuous real integrands are Riemann integrable on compact intervals. A continuous function on is Riemann integrable, by Heine-Cantor and Riemann's criterion.
Integrable derivatives integrate to their endpoint differences. The second fundamental theorem: if is differentiable on with and is integrable, then .
Integration by parts holds for continuously differentiable real functions on compact intervals. If are differentiable on with integrable, then .
Under countable choice the compact Riemann and Lebesgue integrals agree. A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral.
Increasing nonnegative truncations converge in integral. Monotone convergence for the integral.
Integration against a density agrees with integration of the product for nonnegative measurable integrands. Integrating against a density agrees with integrating the product.
Finite first absolute moment permits differentiation of the characteristic function. Moments give derivatives of the characteristic function.
An integrable absolute majorant permits complex integral limits. Dominated convergence.
Euler form has unit modulus on imaginary arguments. , , and .
The sine and cosine derivatives justify real-component integration by parts. The derivatives of sine and cosine are cosine and minus sine.
A real function with zero derivative on an interval is constant. A function continuous on an interval whose derivative vanishes at every interior point of is constant on ; consequently two such functions with the same derivative differ by a constant.
Affine changes give the stated characteristic-function transformation. Characteristic functions under affine maps and independent sums.
The exponential addition law holds, and the complex exponential extends the real exponential. , and the complex exponential extends the real exponential.
Real integrals are defined through positive and negative parts, and complex integrals through real and imaginary parts. Integrable real and complex functions, and their integrals.
The real exponential is defined by the everywhere convergent series . The real exponential function and the number by a power series.
Proof
Given: Assume AC. If has law with , then for every real . Moreover and , including .
Write and let be the coordinate under its probability law. By [F1]–[F2], this is a probability law with density . For any measurable complex with , apply [F11] to the positive and negative parts of and . The definitions in [F19] then give ; in particular, every density-integral identity used below is covered. The derivative rules give . All compact-interval functions below are continuously differentiable, so [F6]–[F9] apply also to each real and imaginary component. AC is used through the normal-law construction and the countable-choice Riemann/Lebesgue bridge; no sequence of arbitrary witnesses is selected.
For , the series in [F20] has nonnegative terms at , so . By [F18], ; hence and both and tend to zero. For each positive integer , FTC on each half interval gives . Thus MCT proves . Also ; DCT with majorant proves . Integration by parts with gives . MCT and [F2] now give . All truncations here use the explicit integers R.
By the finite first moment and [F12], . On , componentwise integration by parts, using [F14]–[F15], gives . The boundary has modulus at most . The two integrands are dominated respectively by and , already integrable. DCT therefore gives for every t, with no improper differentiation left unjustified.
By the real-component product and chain rules, has derivative zero. Apply [F16] to its real and imaginary parts on every real interval. Since , for all t, hence . For in law, [F17] yields , and [F18] combines the exponents. Its moments follow by expanding the finite integrable expressions: and . For the variable equals m almost surely and both formulas give the Dirac law directly.
Depends on
- Standard normal and normal laws
- The standard normal density has total mass one
- 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)$
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- A continuous function on $[a,b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion
- 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)$
- If $u,v$ are differentiable on $[a,b]$ with $u',v'$ integrable, then $\int_a^b u v' = u(b)v(b)-u(a)v(a) - \int_a^b u'v$
- A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral
- Monotone convergence for the integral
- Integrating against a density agrees with integrating the product
- Integrable real and complex functions, and their integrals
- Moments give derivatives of the characteristic function
- Dominated convergence
- $\exp(x+iy)=e^x(\cos y+i\sin y)$, $|\exp(x+iy)|=e^x$, and $e^{i\pi}+1=0$
- The derivatives of sine and cosine are cosine and minus sine
- A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$; consequently two such functions with the same derivative differ by a constant
- Characteristic functions under affine maps and independent sums
- $\exp(z+w)=\exp z\,\exp w$, and the complex exponential extends the real exponential
- The real exponential function and the number $e$ by a power series
- The Lebesgue integral is linear on $L^1(\mu)$
- The Axiom of Choice
Used by
- Feller negligibility cannot be removed from the converse Counterexample
- Multivariate normal law, including singular covariance Definition
- A degenerate multivariate Gaussian limit Example
- Characteristic function of a multivariate normal law Lemma
- Feller converse to Lindeberg-Feller Theorem
- Lindeberg-Feller central limit theorem: sufficiency Theorem
- Lindeberg-Levy iid central limit theorem Theorem
Dependency tree · two levels
117 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 3.3.5 (standard reference, not scraped)
- Norris, Probability and Measure, Section 8 (standard reference, not scraped)