dimH_range_le — Mathlib

English

For a HölderWith map, the Hausdorff dimension of its range is bounded by the domain's dimension divided by r.

Русский

Для отображения HölderWith размерность Хаусдорфа образа ограничена размерностью домена, делённой на r.

LaTeX

$$$$\\dimH(\\operatorname{range} f) \\leq \\frac{\\dimH(\\operatorname{univ})}{r}.$$$$

Lean4

/-- If `f` is a Hölder continuous map with exponent `r > 0`, then the Hausdorff dimension of its
range is at most the Hausdorff dimension of its domain divided by `r`. -/
theorem dimH_range_le (h : HolderWith C r f) (hr : 0 < r) : dimH (range f) ≤ dimH (univ : Set X) / r :=
  @image_univ _ _ f ▸ h.dimH_image_le hr univ

Похожие утверждения