English
Let d ≥ 0, x ∈ P, c ≠ 0 in the underlying field, and s ⊆ P. The preimage of s under the homothety h(x,c) has Hausdorff measure μ_H[d] scaled by ||c||^{-d}: μ_H[d](AffineMap.homothety x c ⁻¹' s) = ||c||_+^{-d} μ_H[d] s.
Русский
Пусть d ≥ 0, x ∈ P, c ≠ 0, и s ⊆ P. Предобраз гомотетии имеет Хаусдорфову меру, умноженную на ||c||^{-d}: μ_H[d](AffineMap.homothety x c ⁻¹' s) = ||c||_+^{-d} μ_H[d] s.
LaTeX
$$$\mu\!\_{H}^{d}(AffineMap.homothety x c ^{-1}' s) = \|c\|_{+}^{-d} \cdot \mu\!\_{H}^{d} s$$$
Lean4
theorem hausdorffMeasure_homothety_preimage {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
change μH[d] (AffineEquiv.homothetyUnitsMulHom x (Units.mk0 c hc) ⁻¹' s) = _
rw [← AffineEquiv.image_symm, AffineEquiv.coe_homothetyUnitsMulHom_apply_symm,
hausdorffMeasure_homothety_image hd x (_ : 𝕜ˣ).isUnit.ne_zero, Units.val_inv_eq_inv_val, Units.val_mk0, nnnorm_inv]
