isTightMeasureSet_iff_tendsto_measure_compl_closedBall

English

Equivalently to the previous, tightening over tail bounds yields tightness.

Русский

Эквивалентно предыдущему: ограничение хвоста приводит к плотности.

LaTeX

$$IsTightMeasureSet S ↔ Tendsto (fun r => ⨆ μ ∈ S, μ (Metric.closedBall x r)^c) atTop (𝓝 0)$$

Lean4

/-- 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 isTightMeasureSet_iff_tendsto_measure_compl_closedBall [ProperSpace E] (x : E) :
    IsTightMeasureSet S ↔ Tendsto (fun r : ℝ ↦ ⨆ μ ∈ S, μ (Metric.closedBall x r)ᶜ) atTop (𝓝 0) :=
  ⟨fun hS ↦ tendsto_measure_compl_closedBall_of_isTightMeasureSet hS x,
    isTightMeasureSet_of_tendsto_measure_compl_closedBall⟩

Похожие утверждения