English
If f is HölderOnWith with exponent r > 0 on s, then dimH (f'' s) ≤ dimH s / r.
Русский
Если отображение f удовлетворяет условию Хольдера с экспонентой r > 0 на множестве s, то dimH образа f(s) не превышает dimH s / r.
LaTeX
$$$$\\dimH(f'' s) \\leq \\frac{\\dimH s}{r}.$$$$
Lean4
/-- If `f` is a Hölder continuous map with exponent `r > 0`, then `dimH (f '' s) ≤ dimH s / r`. -/
theorem dimH_image_le (h : HolderOnWith C r f s) (hr : 0 < r) : dimH (f '' s) ≤ dimH s / r :=
by
borelize X Y
refine dimH_le fun d hd => ?_
have := h.hausdorffMeasure_image_le hr d.coe_nonneg
rw [hd, ← ENNReal.coe_rpow_of_nonneg _ d.coe_nonneg, top_le_iff] at this
have Hrd : μH[(r * d : ℝ≥0)] s = ⊤ := by
contrapose this
finiteness
rw [ENNReal.le_div_iff_mul_le, mul_comm, ← ENNReal.coe_mul]
exacts [le_dimH_of_hausdorffMeasure_eq_top Hrd, Or.inl (mt ENNReal.coe_eq_zero.1 hr.ne'), Or.inl ENNReal.coe_ne_top]
