English
The 0-dimensional Hausdorff measure of any singleton is 1.
Русский
0-мерная мера Хаусдорфа одиночному множеству равна 1.
LaTeX
$$$\mu_H^{0}({x}) = 1$$$
Lean4
@[simp]
theorem hausdorffMeasure_zero_singleton (x : X) : μH[0] ({ x } : Set X) = 1 :=
by
apply le_antisymm
· let r : ℕ → ℝ≥0∞ := fun _ => 0
let t : ℕ → Unit → Set X := fun _ _ => { x }
have ht : ∀ᶠ n in atTop, ∀ i, diam (t n i) ≤ r n := by
simp only [t, r, imp_true_iff, diam_singleton, eventually_atTop, nonpos_iff_eq_zero, exists_const]
simpa [t, liminf_const] using hausdorffMeasure_le_liminf_sum 0 { x } r tendsto_const_nhds t ht
· rw [hausdorffMeasure_apply]
suffices
(1 : ℝ≥0∞) ≤
⨅ (t : ℕ → Set X) (_ : { x } ⊆ ⋃ n, t n) (_ : ∀ n, diam (t n) ≤ 1),
∑' n, ⨆ _ : (t n).Nonempty, diam (t n) ^ (0 : ℝ)
by
apply le_trans this _
convert le_iSup₂ (α := ℝ≥0∞) (1 : ℝ≥0∞) zero_lt_one
rfl
simp only [ENNReal.rpow_zero, le_iInf_iff]
intro t hst _
rcases mem_iUnion.1 (hst (mem_singleton x)) with ⟨m, hm⟩
have A : (t m).Nonempty := ⟨x, hm⟩
calc
(1 : ℝ≥0∞) = ⨆ h : (t m).Nonempty, 1 := by simp only [A, ciSup_pos]
_ ≤ ∑' n, ⨆ h : (t n).Nonempty, 1 := ENNReal.le_tsum _
