isTightMeasureSet_of_tendsto_measure_compl_closedBall

English

A tight set S is characterized by the tail tending to zero for closed balls around any point.

Русский

Плотность множества S характеризуется тем, что хвост по замкнутым шарам вокруг любой точки стремится к нулю.

LaTeX

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

Lean4

theorem isTightMeasureSet_of_tendsto_measure_compl_closedBall [ProperSpace E] {x : E}
    (h : Tendsto (fun r : ℝ ↦ ⨆ μ ∈ S, μ (Metric.closedBall x r)ᶜ) atTop (𝓝 0)) : IsTightMeasureSet S :=
  by
  refine IsTightMeasureSet_iff_exists_isCompact_measure_compl_le.mpr fun ε hε ↦ ?_
  rw [ENNReal.tendsto_atTop_zero] at h
  obtain ⟨r, h⟩ := h ε hε
  exact ⟨Metric.closedBall x r, isCompact_closedBall x r, by simpa using h r le_rfl⟩

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