English
For the 1-dimensional Hausdorff measure in a normed space, mapping along a line segment scales the measure by the end-to-end distance: μ_H[1](AffineMap.lineMap x y '' s) = d(x,y) · μ_H[1] s, where d is the distance between x and y.
Русский
Для 1-мерной Хаусдорфовой меры в нормированном пространстве отображение вдоль отрезка масштабирует меру пропорционально расстоянию между концами: μ_H^1(lineMap x y '' s) = d(x,y) · μ_H^1(s).
LaTeX
$$$\mu\!\_{H}^{1}(AffineMap.lineMap x y '' s) = \mathrm{nndist}(x,y) \cdot \mu\!\_{H}^{1}(s)$$$
Lean4
/-- Mapping a set of reals along a line segment scales the measure by the length of a segment.
This is an auxiliary result used to prove `hausdorffMeasure_affineSegment`. -/
theorem hausdorffMeasure_lineMap_image (x y : P) (s : Set ℝ) :
μH[1] (AffineMap.lineMap x y '' s) = nndist x y • μH[1] s :=
by
suffices μH[1] (IsometryEquiv.vaddConst x '' ((· • (y -ᵥ x)) '' s)) = nndist x y • μH[1] s by
simpa only [Set.image_image]
borelize E
rw [IsometryEquiv.hausdorffMeasure_image, hausdorffMeasure_smul_right_image, nndist_eq_nnnorm_vsub' E]
