Theorems · Theorem · measure theory

MeasureTheory.iteratedFDeriv_charFun

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

Defined in

Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Cited by

1 results in Mathlib

Foundations

Depth 268 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceSecondCountableTopologyMeasureTheory.IsFiniteMeasure