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.
Second-order characteristic-function expansion
Statement
If and , then as . No third moment or choice axiom is assumed. The same scalar estimates give for every real u. More precisely, for ,
Facts & Assumptions
Real Taylor remainders are bounded by the uniform next derivative bound. A uniform derivative bound gives a uniform Taylor remainder bound.
Sine and cosine have derivatives of all orders bounded by one. The derivatives of sine and cosine are cosine and minus sine.
Euler form has real cosine and imaginary sine components. , , and .
DCT applies to the prescribed nonnegative majorant sequence below. Dominated convergence.
Integrable real and complex linear combinations commute with integration. The Lebesgue integral is linear on .
The characteristic function is the expectation of the unit exponential. Characteristic function of a real random variable.
Proof
Given: If and , then as . No third moment or choice axiom is assumed. The same scalar estimates give for every real u. More precisely, for ,
Taylor at zero through degree two for cosine and sine, with third derivatives bounded by one, gives and . Euler form and the triangle inequality give . Taylor through degree one gives and , hence . Adding bounds for all real u. At u=0 all remainders vanish.
For , the first step gives . This is a measurable nonnegative sequence tending pointwise to zero, bounded by the integrable . DCT therefore makes its expectations tend to zero. The bound is uniform over all such t, so as a genuine two-sided real limit, without choosing a sequence of frequencies or requiring . Also gives integrability of the linear term.
By linearity, . Insert the stated moments and the preceding remainder limit. If , the same majorants have zero integral, so the remainder vanishes and the formula still holds. At t=0 the defining expectation is one. Every limiting integrand was explicitly specified; no choice principle enters.
Depends on
- A uniform derivative bound gives a uniform Taylor remainder bound
- The derivatives of sine and cosine are cosine and minus sine
- $\exp(x+iy)=e^x(\cos y+i\sin y)$, $|\exp(x+iy)|=e^x$, and $e^{i\pi}+1=0$
- Dominated convergence
- The Lebesgue integral is linear on $L^1(\mu)$
- Characteristic function of a real random variable
- Moments, variance, and covariance on a probability space
Used by
Dependency tree · two levels
32 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
- Aldous and Chewi, Probability Theory notes, Lemmas 5.4-5.5 (standard reference, not scraped)
- Varadhan, Probability Theory, Chapter 3, Section 3.6 (standard reference, not scraped)