hausdorffMeasure_image_le — Mathlib

English

For any nonzero scalar r in a normed space E, μH^d(r·s) = ||r||^d μH^d(s) for d ≥ 0.

Русский

Для нерезного скаляра r и множества s в нормированном пространстве: μ_H^d(r·s) = ||r||^d μ_H^d(s) при d ≥ 0.

LaTeX

$$$d \ge 0 \Rightarrow μ_H^{d}(r\cdot s) = \|r\|^{d} μ_H^{d}(s) \quad (r \neq 0)$$$

Lean4

/-- If `f : X → Y` is `K`-Lipschitz on `s`, then `μH[d] (f '' s) ≤ K ^ d * μH[d] s`. -/
theorem hausdorffMeasure_image_le (h : LipschitzOnWith K f s) {d : ℝ} (hd : 0 ≤ d) :
    μH[d] (f '' s) ≤ (K : ℝ≥0∞) ^ d * μH[d] s := by
  simpa only [NNReal.coe_one, one_mul] using h.holderOnWith.hausdorffMeasure_image_le zero_lt_one hd

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