Documentation

Mathlib.MeasureTheory.Measure.TightNormed

Tight sets of measures in normed spaces #

Criteria for tightness of sets of measures in normed and inner product spaces.

Main statements #

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.

In a proper normed group, a set of measures S is tight if and only if the function r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖} tends to 0 at infinity.

theorem MeasureTheory.isTightMeasureSet_of_forall_basis_tendsto {E : Type u_1} {mE : MeasurableSpace E} {S : Set (Measure E)} [NormedAddCommGroup E] {𝕜 : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Fintype ι] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (b : OrthonormalBasis ι 𝕜 E) (h : ∀ (i : ι), Filter.Tendsto (fun (r : ) => μS, μ {x : E | r < inner (b i) x}) Filter.atTop (nhds 0)) :
theorem MeasureTheory.isTightMeasureSet_of_inner_tendsto {E : Type u_1} {mE : MeasurableSpace E} {S : Set (Measure E)} [NormedAddCommGroup E] {𝕜 : Type u_2} [RCLike 𝕜] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (h : ∀ (y : E), Filter.Tendsto (fun (r : ) => μS, μ {x : E | r < inner y x}) Filter.atTop (nhds 0)) :
theorem MeasureTheory.isTightMeasureSet_iff_inner_tendsto {E : Type u_1} {mE : MeasurableSpace E} {S : Set (Measure E)} [NormedAddCommGroup E] (𝕜 : Type u_2) [RCLike 𝕜] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
IsTightMeasureSet S ∀ (y : E), Filter.Tendsto (fun (r : ) => μS, μ {x : E | 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.