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.
• isTightMeasureSet_range_iff_tendsto_limsup_measure_norm_gt: in a proper normed group, the range of a sequence of measures μ : ℕ → Measure E is tight if and only if the function r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖x‖}) atTop tends to 0 at infinity.
• isTightMeasureSet_range_iff_tendsto_limsup_inner: in a finite-dimensional inner product space, the range of a sequence of measures μ : ℕ → Measure E is tight if and only if the function r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖⟪y, x⟫_𝕜‖}) atTop 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_range_of_tendsto_limsup_measure_norm_gt {E : Type u_1} {mE : MeasurableSpace E} [NormedAddCommGroup E] [BorelSpace E] [ProperSpace E] {μ : ℕ → Measure E} [∀ (i : ℕ), IsFiniteMeasure (μ i)] (h : Filter.Tendsto (fun (r : ℝ) => Filter.limsup (fun (n : ℕ) => (μ n) {x : E | r < ‖x‖}) Filter.atTop) Filter.atTop (nhds 0)) : IsTightMeasureSet (Set.range μ)

For a sequence of measures indexed by ℕ, if the function r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖x‖}) atTop tends to 0 at infinity, then the set of measures in the sequence is tight. Compared to isTightMeasureSet_of_tendsto_measure_norm_gt, this lemma replaces a supremum over all measures by a limsup. This is possible because the sequence is indexed by ℕ.

theorem MeasureTheory.isTightMeasureSet_range_iff_tendsto_limsup_measure_norm_gt {E : Type u_1} {mE : MeasurableSpace E} [NormedAddCommGroup E] [BorelSpace E] [ProperSpace E] {μ : ℕ → Measure E} [∀ (i : ℕ), IsFiniteMeasure (μ i)] : IsTightMeasureSet (Set.range μ) ↔ Filter.Tendsto (fun (r : ℝ) => Filter.limsup (fun (n : ℕ) => (μ n) {x : E | r < ‖x‖}) Filter.atTop) Filter.atTop (nhds 0)

For a sequence of measures indexed by ℕ, the set of measures in the sequence is tight if and only if the function r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖x‖}) atTop tends to 0 at infinity. Compared to isTightMeasureSet_iff_tendsto_measure_norm_gt, this lemma replaces a supremum over all measures by a limsup. This is possible because the sequence is indexed by ℕ.

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.

theorem MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_inner {E : Type u_1} {mE : MeasurableSpace E} [NormedAddCommGroup E] (𝕜 : Type u_2) [RCLike 𝕜] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [BorelSpace E] {μ : ℕ → Measure E} [∀ (i : ℕ), IsFiniteMeasure (μ i)] (h : ∀ (y : E), Filter.Tendsto (fun (r : ℝ) => Filter.limsup (fun (n : ℕ) => (μ n) {x : E | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop (nhds 0)) : IsTightMeasureSet (Set.range μ)

theorem MeasureTheory.isTightMeasureSet_range_iff_tendsto_limsup_inner {E : Type u_1} {mE : MeasurableSpace E} [NormedAddCommGroup E] (𝕜 : Type u_2) [RCLike 𝕜] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [BorelSpace E] {μ : ℕ → Measure E} [∀ (i : ℕ), IsFiniteMeasure (μ i)] : IsTightMeasureSet (Set.range μ) ↔ ∀ (y : E), Filter.Tendsto (fun (r : ℝ) => Filter.limsup (fun (n : ℕ) => (μ n) {x : E | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop (nhds 0)

In a finite-dimensional inner product space, the range of a sequence of measures μ : ℕ → Measure E is tight if and only if the function r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖⟪y, x⟫_𝕜‖}) atTop tends to 0 at infinity for all y.

theorem MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_inner_of_norm_eq_one {E : Type u_1} {mE : MeasurableSpace E} [NormedAddCommGroup E] (𝕜 : Type u_2) [RCLike 𝕜] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [BorelSpace E] {μ : ℕ → Measure E} [∀ (i : ℕ), IsFiniteMeasure (μ i)] (h : ∀ (y : E), ‖y‖ = 1 → Filter.Tendsto (fun (r : ℝ) => Filter.limsup (fun (n : ℕ) => (μ n) {x : E | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop (nhds 0)) : IsTightMeasureSet (Set.range μ)

theorem MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_measureReal_inner_of_norm_eq_one {E : Type u_1} {mE : MeasurableSpace E} [NormedAddCommGroup E] (𝕜 : Type u_2) [RCLike 𝕜] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [BorelSpace E] {μ : ℕ → Measure E} [∀ (i : ℕ), IsFiniteMeasure (μ i)] (h : ∀ (y : E), ‖y‖ = 1 → Filter.Tendsto (fun (r : ℝ) => Filter.limsup (fun (n : ℕ) => (μ n).real {x : E | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop (nhds 0)) (C : NNReal) (hμ : ∀ᶠ (n : ℕ) in Filter.atTop, (μ n) Set.univ ≤ ↑C) : IsTightMeasureSet (Set.range μ)