le_hausdorffMeasure_image — Mathlib

English

If f is antilipschitz with constant K, then μH^d(s) ≤ K^d μH^d(f(s)).

Русский

Если f антилипшиц с константой K, то μ_H^d(s) ≤ K^d μ_H^d(f(s)).

LaTeX

$$$\mu_H^{d}(s) \le (K)^{d} \mu_H^{d}(f''s)$$$

Lean4

theorem le_hausdorffMeasure_image (hf : AntilipschitzWith K f) (hd : 0 ≤ d) (s : Set X) :
    μH[d] s ≤ (K : ℝ≥0∞) ^ d * μH[d] (f '' s) :=
  calc
    μH[d] s ≤ μH[d] (f ⁻¹' (f '' s)) := measure_mono (subset_preimage_image _ _)
    _ ≤ (K : ℝ≥0∞) ^ d * μH[d] (f '' s) := hf.hausdorffMeasure_preimage_le hd (f '' s)

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