English
Let E be a normed additive group and v an element of E. For any subset S of the real line, the 1-dimensional Hausdorff measure of the image of S under the map r ↦ r v equals the length of v times the Hausdorff measure of S: μ_H^1((r ↦ r·v)''S) = ||v||_+ · μ_H^1(S).
Русский
Пусть E — нормывая аддитивная группа, пусть v ∈ E. Для любой подмножества S ⊆ ℝ выполнено: Хаусдорфова мера размерности 1 изображение S под отображением r ↦ r·v умножается на длину v: μ_H^1((r ↦ r·v)''S) = ||v||_+ · μ_H^1(S).
LaTeX
$$$\mu\!\_{H}^{1}((\lambda r, r \cdot v) '' s) = \|v\|_{+} \cdot \mu\!\_{H}^{1}(s)$$$
Lean4
theorem hausdorffMeasure_smul_right_image [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
(v : E) (s : Set ℝ) : μH[1] ((fun r => r • v) '' s) = ‖v‖₊ • μH[1] s :=
by
obtain rfl | hv := eq_or_ne v 0
· haveI := noAtoms_hausdorff E one_pos
obtain rfl | hs := s.eq_empty_or_nonempty
· simp
simp [hs]
have hn : ‖v‖ ≠ 0 := norm_ne_zero_iff.mpr hv
suffices μH[1] ((‖v‖ • ·) '' (LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v) '' s)) = ‖v‖₊ • μH[1] s by
simpa only [Set.image_image, smul_comm (norm _), inv_smul_smul₀ hn, LinearMap.toSpanSingleton_apply] using this
have iso_smul : Isometry (LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) :=
by
refine AddMonoidHomClass.isometry_of_norm _ fun x => (norm_smul _ _).trans ?_
rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hn, mul_one, LinearMap.id_apply]
rw [Set.image_smul, Measure.hausdorffMeasure_smul₀ zero_le_one hn, nnnorm_norm, NNReal.rpow_one,
iso_smul.hausdorffMeasure_image (Or.inl <| zero_le_one' ℝ)]
