Theorems · Theorem · measure theory

MeasureTheory.isTightMeasureSet_iff_inner_tendsto

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

In a finite-dimensional inner product space, a set of measures S is tight if and only if the function r ↦ ⨆ μ ∈ S, μ {x | r < |⟪y, x⟫|} tends to 0 at infinity for all y.

Defined in

Mathlib.MeasureTheory.Measure.TightNormed

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupRCLikeInnerProductSpaceFiniteDimensional