hausdorffMeasure_le_liminf_tsum — Mathlib

English

Hausdorff measure satisfies a liminf bound via a sequence of coverings with diameters going to 0.

Русский

Хаусдорфова мера удовлетворяет ограничению по лим инф via последовательности покрытий с диами, сходящимися к нулю.

LaTeX

$$$ μH[d] s \le \liminf (\sum_i diam(t_n i)^d) $$$

Lean4

/-- To bound the Hausdorff measure of a set, one may use coverings with maximum diameter tending
to `0`, indexed by any sequence of countable types. -/
theorem hausdorffMeasure_le_liminf_tsum {β : Type*} {ι : β → Type*} [∀ n, Countable (ι n)] (d : ℝ) (s : Set X)
    {l : Filter β} (r : β → ℝ≥0∞) (hr : Tendsto r l (𝓝 0)) (t : ∀ n : β, ι n → Set X)
    (ht : ∀ᶠ n in l, ∀ i, diam (t n i) ≤ r n) (hst : ∀ᶠ n in l, s ⊆ ⋃ i, t n i) :
    μH[d] s ≤ liminf (fun n => ∑' i, diam (t n i) ^ d) l :=
  mkMetric_le_liminf_tsum s r hr t ht hst _

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