Theorems · Theorem · probability

MeasureTheory.ProbabilityMeasure.tendsto_of_tendsto_charFun

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {μ₀ : MeasureTheory.ProbabilityMeasure E}
  {μ : ℕ → MeasureTheory.ProbabilityMeasure E},
  (∀ (t : E),
      Filter.Tendsto (fun n => MeasureTheory.charFun (↑(μ n)) t) Filter.atTop (nhds (MeasureTheory.charFun (↑μ₀) t))) →
    Filter.Tendsto μ Filter.atTop (nhds μ₀)

If the characteristic functions of a sequence of probability measures converge pointwise to the characteristic function of a probability measure, then the measures converge weakly.

Defined in

Mathlib.MeasureTheory.Measure.LevyConvergence

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpace