A characteristic-function moment method

The project only needs the one-dimensional Cramér--Wold form of the Gaussian moment method. This file derives it directly from Taylor's theorem for characteristic functions. An even moment controls the Taylor remainder uniformly, so convergence of all raw moments to a Gaussian law implies convergence of the characteristic function.

noncomputable def Anderson4D.momentPolynomialOne (μ : MeasureTheory.Measure ℝ) (N : ℕ) : ℂ

The degree-N-1 Taylor polynomial at frequency one, written in terms of the first N raw moments.

Equations

• Anderson4D.momentPolynomialOne μ N = ∑ k ∈ Finset.range N, (↑k.factorial)⁻¹ * Complex.I ^ k * ↑(∫ (x : ℝ), x ^ k ∂μ)

theorem Anderson4D.norm_iteratedDeriv_charFun_le_evenMoment (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (q : ℕ) (hmem : MeasureTheory.MemLp id (↑(2 * q)) μ) (t : ℝ) : ‖iteratedDeriv (2 * q) (MeasureTheory.charFun μ) t‖ ≤ ∫ (x : ℝ), x ^ (2 * q) ∂μ

The norm of the 2q-th derivative of a characteristic function is bounded by the corresponding even raw moment.

theorem Anderson4D.norm_charFun_one_sub_momentPolynomial_le (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (q : ℕ) (hmem : MeasureTheory.MemLp id (↑(2 * (q + 1))) μ) : ‖MeasureTheory.charFun μ 1 - momentPolynomialOne μ (2 * (q + 1))‖ ≤ (∫ (x : ℝ), x ^ (2 * (q + 1)) ∂μ) / ↑(2 * q + 1).factorial

Taylor's theorem at frequency one, with the remainder controlled by one even moment. The polynomial contains all degrees below 2(q+1).

theorem Anderson4D.tendsto_momentPolynomialOne {ι : Type u_1} {l : Filter ι} (μ : ι → MeasureTheory.Measure ℝ) (μ₀ : MeasureTheory.Measure ℝ) (N : ℕ) (hmom : ∀ (n : ℕ), Filter.Tendsto (fun (i : ι) => ∫ (x : ℝ), x ^ n ∂μ i) l (nhds (∫ (x : ℝ), x ^ n ∂μ₀))) : Filter.Tendsto (fun (i : ι) => momentPolynomialOne (μ i) N) l (nhds (momentPolynomialOne μ₀ N))

Convergence of finitely many raw moments gives convergence of the corresponding characteristic-function Taylor polynomials.

theorem Anderson4D.tendsto_charFun_one_of_moments {ι : Type u_1} {l : Filter ι} (μ : ι → MeasureTheory.Measure ℝ) (μ₀ : MeasureTheory.Measure ℝ) [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] [MeasureTheory.IsFiniteMeasure μ₀] (hmem : ∀ (i : ι) (n : ℕ), MeasureTheory.MemLp id (↑n) (μ i)) (hmem₀ : ∀ (n : ℕ), MeasureTheory.MemLp id (↑n) μ₀) (hmom : ∀ (n : ℕ), Filter.Tendsto (fun (i : ι) => ∫ (x : ℝ), x ^ n ∂μ i) l (nhds (∫ (x : ℝ), x ^ n ∂μ₀))) (htail : Filter.Tendsto (fun (q : ℕ) => (∫ (x : ℝ), x ^ (2 * (q + 1)) ∂μ₀) / ↑(2 * q + 1).factorial) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (i : ι) => MeasureTheory.charFun (μ i) 1) l (nhds (MeasureTheory.charFun μ₀ 1))

One-dimensional Gaussian moment method, characteristic-function form. If all raw moments converge and the even-moment Taylor remainder of the target tends to zero, then the characteristic functions converge at frequency one.

The tail premise is precisely what Gaussian moment determinacy supplies; it is separated so this theorem is reusable for any moment-determinate target law.

theorem Anderson4D.gaussianPairingCount_succ_div_oddFactorial (q : ℕ) : ↑(gaussianPairingCount (q + 1)) / ↑(2 * q + 1).factorial = 1 / (2 ^ q * ↑q.factorial)

The double-factorial pairing count divided by the adjacent odd factorial. This is the factorial gain behind Gaussian moment determinacy.

theorem Anderson4D.centeredGaussianMoment_tail_tendsto_zero (v : NNReal) : Filter.Tendsto (fun (q : ℕ) => centeredGaussianMoment v (2 * (q + 1)) / ↑(2 * q + 1).factorial) Filter.atTop (nhds 0)

The Taylor remainders supplied by the even moments of a centered Gaussian tend to zero.

theorem Anderson4D.tendsto_charFun_one_of_moments_gaussian {ι : Type u_1} {l : Filter ι} (μ : ι → MeasureTheory.Measure ℝ) [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] (v : NNReal) (hmem : ∀ (i : ι) (n : ℕ), MeasureTheory.MemLp id (↑n) (μ i)) (hmom : ∀ (n : ℕ), Filter.Tendsto (fun (i : ι) => ∫ (x : ℝ), x ^ n ∂μ i) l (nhds (centeredGaussianMoment v n))) : Filter.Tendsto (fun (i : ι) => MeasureTheory.charFun (μ i) 1) l (nhds (MeasureTheory.charFun (ProbabilityTheory.gaussianReal 0 v) 1))

Gaussian specialization of tendsto_charFun_one_of_moments.