hausdorffMeasure_image_le — Mathlib

English

If f is Hölder on s with C,r, then μH^d(f(s)) ≤ C^d μH^{r d}(s) for all d with hd≥0.

Русский

Если f Hölder на s с константой C и показателем r, тогда для всех d ≥ 0 выполняется μ_H^d(f(s)) ≤ C^d μ_H^{r d}(s).

LaTeX

$$$h :\; \text{HolderOnWith } C\, r\, f\, s \Rightarrow \forall d\ge 0:\; μ_H^{d}(f''s) ≤ (C)^{d} μ_H^{r d}(s)$$$

Lean4

/-- If `f` is a `K`-Lipschitz map, then it increases the Hausdorff `d`-measures of sets at most
by the factor of `K ^ d`. -/
theorem hausdorffMeasure_image_le (h : LipschitzWith K f) {d : ℝ} (hd : 0 ≤ d) (s : Set X) :
    μH[d] (f '' s) ≤ (K : ℝ≥0∞) ^ d * μH[d] s :=
  h.lipschitzOnWith.hausdorffMeasure_image_le hd

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