English
The Hausdorff dimension is the supremum of the limit superior of dimH along small sets around points of s.
Русский
Размерность Хаусдорфа равна супремуму предела верхних пределoв dimH вдоль малых множеств вокруг точек s.
LaTeX
$$$$\\bigl(\\sup_{x \\in s} \\limsup \\dimH (\\mathcal{N}_s(x).smallSets)\\bigr) = \\dimH s.$$$$
Lean4
/-- In an (extended) metric space with second countable topology, the Hausdorff dimension
of a set `s` is the supremum over `x ∈ s` of the limit superiors of `dimH t` along
`(𝓝[s] x).smallSets`. -/
theorem bsupr_limsup_dimH (s : Set X) : ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets = dimH s :=
by
refine le_antisymm (iSup₂_le fun x _ => ?_) ?_
· refine limsup_le_of_le isCobounded_le_of_bot ?_
exact eventually_smallSets.2 ⟨s, self_mem_nhdsWithin, fun t => dimH_mono⟩
· refine le_of_forall_lt_imp_le_of_dense fun r hr => ?_
rcases exists_mem_nhdsWithin_lt_dimH_of_lt_dimH hr with ⟨x, hxs, hxr⟩
refine le_iSup₂_of_le x hxs ?_; rw [limsup_eq]; refine le_sInf fun b hb => ?_
rcases eventually_smallSets.1 hb with ⟨t, htx, ht⟩
exact (hxr t htx).le.trans (ht t Subset.rfl)
