Alphabeta Math
LemmaStatement: AI-adaptedProof: 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.

Second-order characteristic-function expansion

Statement

If EX=0 and EX2=σ2<, then φX(t)=1σ2t2/2+o(t2) as t0. No third moment or choice axiom is assumed. The same scalar estimates give 01cosuu2/2 for every real u. More precisely, for r(u)=eiu1iu+u2/2, r(u)min(u3/3,4u2),eiu1iuu2.

Facts & Assumptions

[F1]

Real Taylor remainders are bounded by the uniform next derivative bound. A uniform derivative bound gives a uniform Taylor remainder bound.

[F2]

Sine and cosine have derivatives of all orders bounded by one. The derivatives of sine and cosine are cosine and minus sine.

[F4]

DCT applies to the prescribed nonnegative majorant sequence below. Dominated convergence.

[F5]

Integrable real and complex linear combinations commute with integration. The Lebesgue integral is linear on L1(μ).

[F6]

The characteristic function is the expectation of the unit exponential. Characteristic function of a real random variable.

Proof

Given: If EX=0 and EX2=σ2<, then φX(t)=1σ2t2/2+o(t2) as t0. No third moment or choice axiom is assumed. The same scalar estimates give 01cosuu2/2 for every real u. More precisely, for r(u)=eiu1iu+u2/2, r(u)min(u3/3,4u2),eiu1iuu2.

1.1

Taylor at zero through degree two for cosine and sine, with third derivatives bounded by one, gives cosu1+u2/2u3/6 and sinuuu3/6. Euler form and the triangle inequality give r(u)u3/3. Taylor through degree one gives cosu1u2/2 and sinuuu2/2, hence eiu1iuu2. Adding u2/2 bounds r(u)3u2/24u2 for all real u. At u=0 all remainders vanish.

F1F2F3
2.1

For 0<t1/n, the first step gives r(tX)/t2X2min(X/(3n),4). This is a measurable nonnegative sequence tending pointwise to zero, bounded by the integrable 4X2. DCT therefore makes its expectations tend to zero. The bound is uniform over all such t, so Er(tX)=o(t2) as a genuine two-sided real limit, without choosing a sequence of frequencies or requiring EX3<. Also X1+X2 gives integrability of the linear term.

step 1.1F4
3.1

By linearity, φX(t)=1+itEXt2EX2/2+Er(tX). Insert the stated moments and the preceding remainder limit. If σ=0, 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.

step 1.1step 2.1F5F6

Depends on

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