Theorems · Theorem · measure theory

MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_measure_norm_gt

∀ {E : Type u_1} {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] [BorelSpace E] [ProperSpace E]
  {μ : ℕ → MeasureTheory.Measure E} [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)],
  Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n) {x | r < ‖x‖}) Filter.atTop) Filter.atTop (nhds 0) →
    MeasureTheory.IsTightMeasureSet (Set.range μ)

For a sequence of measures indexed by ℕ, if the function r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖x‖}) atTop tends to 0 at infinity, then the set of measures in the sequence is tight. Compared to isTightMeasureSet_of_tendsto_measure_norm_gt, this lemma replaces a supremum over all measures by a limsup. This is possible because the sequence is indexed by ℕ.

Defined in

Mathlib.MeasureTheory.Measure.TightNormed

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupBorelSpaceProperSpaceMeasureTheory.IsFiniteMeasure