English
Let d be a nonnegative real number, x a point in a normed space P, c a nonzero scalar in a field, and s a subset of P. Then applying a homothety (dilation) with center x and factor c scales the d-dimensional Hausdorff measure by ||c||^d: μ_H[d](AffineMap.homothety x c '' s) = ||c||_+^d · μ_H[d] s.
Русский
Пусть d ≥ 0, x ∈ P, c ≠ 0 в поле, и s ⊆ P. Гомотетия (однородное масштабирование) с центром x и коэффициентом c умножает d-мерную Хаусдорфову меру на ||c||^d: μ_H[d](AffineMap.homothety x c '' s) = ||c||_+^d · μ_H[d] s.
LaTeX
$$$\mu\!\_{H}^{d}(AffineMap.homothety\\ x\\ c '' s) = \|c\\|_{+}^{d} \cdot \mu\!\_{H}^{d} s$$$
Lean4
/-- Scaling by `c` around `x` scales the measure by `‖c‖₊ ^ d`. -/
theorem hausdorffMeasure_homothety_image {d : ℝ} (hd : 0 ≤ d) (x : P) {c : 𝕜} (hc : c ≠ 0) (s : Set P) :
μH[d] (AffineMap.homothety x c '' s) = ‖c‖₊ ^ d • μH[d] s :=
by
suffices
μH[d] (IsometryEquiv.vaddConst x '' ((c • ·) '' ((IsometryEquiv.vaddConst x).symm '' s))) = ‖c‖₊ ^ d • μH[d] s by
simpa only [Set.image_image]
borelize E
rw [IsometryEquiv.hausdorffMeasure_image, Set.image_smul, Measure.hausdorffMeasure_smul₀ hd hc,
IsometryEquiv.hausdorffMeasure_image]
