Theorems · Theorem · measure theory

MeasureTheory.isTightMeasureSet_range_iff_tendsto_limsup_inner

∀ {E : Type u_1} {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] (𝕜 : Type u_2) [inst_1 : RCLike 𝕜]
  [inst_2 : InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [BorelSpace E] {μ : ℕ → MeasureTheory.Measure E}
  [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)],
  MeasureTheory.IsTightMeasureSet (Set.range μ) ↔
    ∀ (y : E),
      Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n) {x | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop
        (nhds 0)

In a finite-dimensional inner product space, the range of a sequence of measures μ : ℕ → Measure E is tight if and only if the function r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖⟪y, x⟫_𝕜‖}) atTop tends to 0 at infinity for all y.

Defined in

Mathlib.MeasureTheory.Measure.TightNormed

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupRCLikeInnerProductSpaceFiniteDimensionalBorelSpaceMeasureTheory.IsFiniteMeasure