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.

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.