tendsto_measure_norm_gt_of_isTightMeasureSet

English

Given tight S, the tail of the norms tends to zero: μ({x : r < ||x||}) → 0 as r → ∞.

Русский

Для плотного S хвост норм стремится к нулю: μ({x : r < ||x||}) → 0 при r → ∞.

LaTeX

$$Tendsto (fun r => ⨆ μ ∈ S, μ {x | r < ‖x‖}) atTop (𝓝 0)$$

Lean4

theorem tendsto_measure_norm_gt_of_isTightMeasureSet (hS : IsTightMeasureSet S) :
    Tendsto (fun r : ℝ ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) atTop (𝓝 0) :=
  by
  have h := tendsto_measure_compl_closedBall_of_isTightMeasureSet hS 0
  convert h using 6 with r
  ext
  simp

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