Theorems · Theorem · probability

ProbabilityTheory.IsGaussian.charFun_eq

∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [BorelSpace E] {μ : MeasureTheory.Measure E} [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

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceProbabilityTheory.IsGaussian