English
If f is locally Hölder on a set s, then the Hausdorff dimension of the image of s is bounded by the dimension of s divided by r.
Русский
Если f локально удовлетворяет условию Хольдера на множестве s, то размерность образа f(s) не превосходит dimH s / r.
LaTeX
$$$$\\dimH(\\operatorname{image} f\, s) \\leq \\frac{\\dimH s}{r}.$$$$
Lean4
/-- If `f : X → Y` is Hölder continuous in a neighborhood of every point `x : X` with the same
positive exponent `r` but possibly different coefficients, then the Hausdorff dimension of the range
of `f` is at most the Hausdorff dimension of `X` divided by `r`. -/
theorem dimH_range_le_of_locally_holder_on [SecondCountableTopology X] {r : ℝ≥0} {f : X → Y} (hr : 0 < r)
(hf : ∀ x : X, ∃ C : ℝ≥0, ∃ s ∈ 𝓝 x, HolderOnWith C r f s) : dimH (range f) ≤ dimH (univ : Set X) / r :=
by
rw [← image_univ]
refine dimH_image_le_of_locally_holder_on hr fun x _ => ?_
simpa only [exists_prop, nhdsWithin_univ] using hf x
