tendsto_measure_compl_closedBall_of_isTightMeasureSet

English

If S is tight, then a certain tail bound as radius grows holds: μ(closedBall(x,r))^c is small as r → ∞.

Русский

Если S плотное, то асимптотически малое значение меры за пределами шара при большом радиусе.

LaTeX

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

Lean4

theorem tendsto_measure_compl_closedBall_of_isTightMeasureSet (hS : IsTightMeasureSet S) (x : E) :
    Tendsto (fun r : ℝ ↦ ⨆ μ ∈ S, μ (Metric.closedBall x r)ᶜ) atTop (𝓝 0) :=
  by
  suffices Tendsto ((⨆ μ ∈ S, μ) ∘ (fun r ↦ (Metric.closedBall x r)ᶜ)) atTop (𝓝 0)
    by
    convert this with r
    simp
  refine hS.comp <| .mono_right ?_ <| monotone_smallSets Metric.cobounded_le_cocompact
  exact (Metric.hasAntitoneBasis_cobounded_compl_closedBall _).tendsto_smallSets

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