Taylor expansion of the characteristic function

This file provides the Taylor expansion of the characteristic function of a measure at 0.

Main statements

• taylorWithinEval_charFun_zero: If a finite measure μ over ℝ admits a moment of order n, then the Taylor expansion of its characteristic function at 0 at order n is given by t ↦ ∑ k ∈ Finset.range (n + 1), (k ! : ℂ)⁻¹ * (t * I) ^ k * ∫ x, x ^ k ∂μ.

Tags

characteristic function, Taylor expansion

theorem MeasureTheory.contDiff_charFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ : Measure E} [IsFiniteMeasure μ] {n : ℕ} (hint : MemLp id (↑n) μ) : ContDiff ℝ (↑n) (charFun μ)

The characteristic function of a finite measure with a moment of order n is C^n. See contDiff_charFun' for the version proving C^∞ by assuming all moments exist.

theorem MeasureTheory.contDiff_charFun' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ : Measure E} [IsFiniteMeasure μ] {n : ℕ∞} (hint : ∀ (k : ℕ), MemLp id (↑k) μ) : ContDiff ℝ (↑n) (charFun μ)

The characteristic function of a measure with all moments is C^∞. See contDiff_charFun for the version proving only C^n by only assuming that the moment of order n exists.

theorem MeasureTheory.continuous_charFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ : Measure E} [IsFiniteMeasure μ] : Continuous (charFun μ)

theorem MeasureTheory.iteratedFDeriv_charFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ : Measure E} [IsFiniteMeasure μ] {n : ℕ} {t : E} (hint : MemLp id (↑n) μ) (x : Fin n → E) : (iteratedFDeriv ℝ n (charFun μ) t) x = Complex.I ^ n * ∫ (y : E), ↑(∏ i : Fin n, inner ℝ y (x i)) * Complex.exp (↑(inner ℝ y t) * Complex.I) ∂μ

theorem MeasureTheory.iteratedDeriv_charFun {μ : Measure ℝ} [IsFiniteMeasure μ] {n : ℕ} {t : ℝ} (hint : MemLp id (↑n) μ) : iteratedDeriv n (charFun μ) t = Complex.I ^ n * ∫ (x : ℝ), ↑x ^ n * Complex.exp (↑t * ↑x * Complex.I) ∂μ

theorem MeasureTheory.iteratedDeriv_charFun_zero {μ : Measure ℝ} [IsFiniteMeasure μ] {n : ℕ} (hint : MemLp id (↑n) μ) : iteratedDeriv n (charFun μ) 0 = Complex.I ^ n * ↑(∫ (x : ℝ), x ^ n ∂μ)

theorem MeasureTheory.taylorWithinEval_charFun_zero {μ : Measure ℝ} [IsFiniteMeasure μ] {n : ℕ} (hint : MemLp id (↑n) μ) (t : ℝ) : taylorWithinEval (charFun μ) n Set.univ 0 t = ∑ k ∈ Finset.range (n + 1), (↑k.factorial)⁻¹ * (↑t * Complex.I) ^ k * ↑(∫ (x : ℝ), x ^ k ∂μ)

theorem MeasureTheory.taylorWithinEval_charFun_two_zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P] {X : Ω → ℝ} (hX : AEMeasurable X P) (hint : MemLp id 2 (Measure.map X P)) (t : ℝ) : taylorWithinEval (charFun (Measure.map X P)) 2 Set.univ 0 t = 1 + ↑(∫ (x : Ω), X x ∂P) * ↑t * Complex.I - ↑(∫ (x : Ω), (X ^ 2) x ∂P) * ↑t ^ 2 / 2

theorem MeasureTheory.taylorWithinEval_charFun_two_zero' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P] {X : Ω → ℝ} (hX : AEMeasurable X P) (h0 : ∫ (x : Ω), X x ∂P = 0) (h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1) (t : ℝ) : taylorWithinEval (charFun (Measure.map X P)) 2 Set.univ 0 t = 1 - ↑t ^ 2 / 2

theorem MeasureTheory.taylor_charFun_two {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P] {X : Ω → ℝ} (hX : AEMeasurable X P) (h0 : ∫ (x : Ω), X x ∂P = 0) (h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1) : (fun (t : ℝ) => charFun (Measure.map X P) t - (1 - ↑t ^ 2 / 2)) =o[nhds 0] fun (t : ℝ) => t ^ 2