dimH_preimage_le — Mathlib

English

If f is antilipschitz with constant K, then the Hausdorff dimension of the preimage of any set is at most the dimension of the set.

Русский

Если отображение антипилешиц с константой K, то размерность Хаусдорфа предобраза любого множества не больше размерности самого множества.

LaTeX

$$$$\\dimH(f^{-1}(s)) \\leq \\dimH(s).$$$$

Lean4

theorem dimH_preimage_le (hf : AntilipschitzWith K f) (s : Set Y) : dimH (f ⁻¹' s) ≤ dimH s :=
  by
  borelize X Y
  refine dimH_le fun d hd => le_dimH_of_hausdorffMeasure_eq_top ?_
  have := hf.hausdorffMeasure_preimage_le d.coe_nonneg s
  rw [hd, top_le_iff] at this
  contrapose! this
  exact ENNReal.mul_ne_top (by simp) this

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