Theorems · Theorem · probability

MeasureTheory.isTightMeasureSet_of_tendsto_charFun

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : ℕ → MeasureTheory.Measure E}
  [∀ (i : ℕ), MeasureTheory.IsProbabilityMeasure (μ i)] {f : E → ℂ},
  ContinuousAt f 0 →
    (∀ (t : E), Filter.Tendsto (fun n => MeasureTheory.charFun (μ n) t) Filter.atTop (nhds (f t))) →
      MeasureTheory.IsTightMeasureSet (Set.range μ)

If the characteristic functions of a sequence of measures μ : ℕ → Measure E converge pointwise to a function which is continuous at 0, then {μ n | n} is tight.

Defined in

Mathlib.MeasureTheory.Measure.LevyConvergence

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpaceMeasureTheory.IsProbabilityMeasure