English
If s is a set in a second countable space X and f is Hölder on each local piece around every x with the same exponent r, then dimH (f'' s) ≤ dimH s / r.
Русский
Если s — множество в пространстве X с двойной счётностью, и f локально удовлетворяет условию Хольдера на каждой окрестности точки x, то dimH образа f(s) ограничена dimH s / r.
LaTeX
$$$$\\dimH\\bigl(\\operatorname{image} f \\, s\\bigr) \\leq \\frac{\\dimH s}{r}.$$$$
Lean4
/-- If `s` is a set in a space `X` with second countable topology and `f : X → Y` is Hölder
continuous in a neighborhood within `s` of every point `x ∈ s` with the same positive exponent `r`
but possibly different coefficients, then the Hausdorff dimension of the image `f '' s` is at most
the Hausdorff dimension of `s` divided by `r`. -/
theorem dimH_image_le_of_locally_holder_on [SecondCountableTopology X] {r : ℝ≥0} {f : X → Y} (hr : 0 < r) {s : Set X}
(hf : ∀ x ∈ s, ∃ C : ℝ≥0, ∃ t ∈ 𝓝[s] x, HolderOnWith C r f t) : dimH (f '' s) ≤ dimH s / r :=
by
choose! C t htn hC using hf
rcases countable_cover_nhdsWithin htn with ⟨u, hus, huc, huU⟩
replace huU := inter_eq_self_of_subset_left huU; rw [inter_iUnion₂] at huU
rw [← huU, image_iUnion₂, dimH_bUnion huc, dimH_bUnion huc]; simp only [ENNReal.iSup_div]
exact iSup₂_mono fun x hx => ((hC x (hus hx)).mono inter_subset_right).dimH_image_le hr
