Theorems · Theorem · measure theory

MeasureTheory.taylorWithinEval_charFun_two_zero

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {X : Ω → ℝ},
  AEMeasurable X P →
    MeasureTheory.MemLp id 2 (MeasureTheory.Measure.map X P) →
      ∀ (t : ℝ),
        taylorWithinEval (MeasureTheory.charFun (MeasureTheory.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

Defined in: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Cited by: 1 results in Mathlib
Foundations: Depth 272 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasureTheory.IsProbabilityMeasure

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites39

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement · cited by 9,879
Complexstatement and proof · cited by 5,565
Finset.sumproof · cited by 5,195
Set.univstatement and proof · cited by 3,945
mul_oneproof · cited by 3,885
one_mulproof · cited by 2,841
Nat.cast_oneproof · cited by 2,501
Nat.cast_zeroproof · cited by 1,870
MeasureTheory.integralstatement and proof · cited by 1,779

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.taylorWithinEval_charFun_two_zero'proof · cited by 1