Theorems · Theorem · measure theory

MeasureTheory.isTightMeasureSet_iff_tendsto_measure_compl_closedBall

∀ {E : Type u_1} {mE : MeasurableSpace E} {S : Set (MeasureTheory.Measure E)} [inst : PseudoMetricSpace E]
  [ProperSpace E] (x : E),
  MeasureTheory.IsTightMeasureSet S ↔
    Filter.Tendsto (fun r => ⨆ μ ∈ S, μ (Metric.closedBall x r)ᶜ) Filter.atTop (nhds 0)

In a proper pseudo-metric space, a set of measures S is tight if and only if the function r ↦ ⨆ μ ∈ S, μ (Metric.closedBall x r)ᶜ tends to 0 at infinity.

Defined in

Mathlib.MeasureTheory.Measure.TightNormed

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceProperSpace