Theorems · Theorem · measure theory

MeasureTheory.isTightMeasureSet_range_of_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)],
  (∀ (y : E),
      Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n) {x | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop
        (nhds 0)) →
    MeasureTheory.IsTightMeasureSet (Set.range μ)

Defined in

Mathlib.MeasureTheory.Measure.TightNormed

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupRCLikeInnerProductSpaceFiniteDimensionalBorelSpaceMeasureTheory.IsFiniteMeasure