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 measuresS
is tight if and only if the functionr ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}
tends to0
at infinity.isTightMeasureSet_iff_inner_tendsto
: in a finite-dimensional inner product space, a set of measuresS
is tight if and only if the functionr ↦ ⨆ μ ∈ S, μ {x | r < |⟪y, x⟫|}
tends to0
at infinity for ally
.
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))
:
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)
:
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))
:
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))
:
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
.