English
For a smooth map f on a finite-dimensional real space, the Hausdorff dimension of the image f(t) does not exceed the dimension of t.
Русский
При гладкой отображении f на конечномерном пространстве Хаусдорфова размерность образа f(t) не превосходит размерности t.
LaTeX
$$dimH( f'' t ) ≤ dimH t$$
Lean4
/-- Let `f` be a function defined on a finite-dimensional real normed space. If `f` is `C¹`-smooth
on a convex set `s`, then the Hausdorff dimension of `f '' s` is less than or equal to the Hausdorff
dimension of `s`.
TODO: do we actually need `Convex ℝ s`? -/
theorem dimH_image_le {f : E → F} {s t : Set E} (hf : ContDiffOn ℝ 1 f s) (hc : Convex ℝ s) (ht : t ⊆ s) :
dimH (f '' t) ≤ dimH t :=
dimH_image_le_of_locally_lipschitzOn fun x hx =>
let ⟨C, u, hu, hf⟩ := (hf x (ht hx)).exists_lipschitzOnWith hc
⟨C, u, nhdsWithin_mono _ ht hu, hf⟩
