Tight sets of measures in normed spaces

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

Main statements

• isTightMeasureSet_iff_tendsto_measure_norm_gt: 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.
• isTightMeasureSet_iff_inner_tendsto: 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.

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

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

theorem MeasureTheory.isTightMeasureSet_iff_tendsto_measure_compl_closedBall {E : Type u_1} {mE : MeasurableSpace E} {S : Set (Measure E)} [PseudoMetricSpace E] [ProperSpace E] (x : E) : 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.

theorem MeasureTheory.tendsto_measure_norm_gt_of_isTightMeasureSet {E : Type u_1} {mE : MeasurableSpace E} {S : Set (Measure E)} [NormedAddCommGroup E] (hS : IsTightMeasureSet S) : Filter.Tendsto (fun (r : ℝ) => ⨆ μ ∈ S, μ {x : E | r < ‖x‖}) Filter.atTop (nhds 0)

theorem MeasureTheory.isTightMeasureSet_of_tendsto_measure_norm_gt {E : Type u_1} {mE : MeasurableSpace E} {S : Set (Measure E)} [NormedAddCommGroup E] [ProperSpace E] (h : Filter.Tendsto (fun (r : ℝ) => ⨆ μ ∈ S, μ {x : E | r < ‖x‖}) Filter.atTop (nhds 0)) : IsTightMeasureSet S

theorem MeasureTheory.isTightMeasureSet_iff_tendsto_measure_norm_gt {E : Type u_1} {mE : MeasurableSpace E} {S : Set (Measure E)} [NormedAddCommGroup E] [ProperSpace E] : IsTightMeasureSet S ↔ Filter.Tendsto (fun (r : ℝ) => ⨆ μ ∈ S, μ {x : E | r < ‖x‖}) Filter.atTop (nhds 0)

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)) : IsTightMeasureSet S

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)) : IsTightMeasureSet S

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.