English
The Hausdorff dimension equals the infimum of all d such that the d-dimensional Hausdorff measure of s is zero.
Русский
Размерность Хаусдорфа равна инфимума всех d, для которых мера Хаусдорфа размерности d нулевая.
LaTeX
$$dimH(s) = \inf_{d \ge 0} \{ d : μH[d](s) = 0 \}$$
Lean4
/-- The Hausdorff dimension of a set `s` is the infimum of all `d : ℝ≥0` such that the
`d`-dimensional Hausdorff measure of `s` is zero. This infimum is taken in `ℝ≥0∞`.
This gives an equivalent definition of the Hausdorff dimension. -/
theorem dimH_eq_iInf (s : Set X) : dimH s = ⨅ (d : ℝ≥0) (_ : μH[d] s = 0), (d : ℝ≥0∞) :=
by
apply le_antisymm
· rw [dimH_def]
simp only [le_iInf_iff, iSup_le_iff, ENNReal.coe_le_coe]
intro i hi j hj
by_contra! hij
simpa [hi, hj] using hausdorffMeasure_mono hij.le s
· by_contra! h
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hdim_lt, hlt⟩
have h0 : μH[d'] s = 0 := hausdorffMeasure_of_dimH_lt hdim_lt
exact hlt.not_ge (iInf₂_le d' h0)
