Theorems · Theorem · probability

ProbabilityTheory.isGaussian_iff_charFun_eq

∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.IsGaussian μ ↔
    ∀ (t : E),
      MeasureTheory.charFun μ t =
        Complex.exp
          ((∫ (x : E), ↑((fun x => inner ℝ t x) x) ∂μ) * Complex.I -
            ↑(ProbabilityTheory.variance (fun x => inner ℝ t x) μ) / 2)

Defined in

Mathlib.Probability.Distributions.Gaussian.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceCompleteSpaceMeasureTheory.IsFiniteMeasure