Commit 2023-06-02 12:04 571e13ca

View on Github →

feat(measure_theory/measure/hausdorff): the 1-measure of a segment is its length (#18981) Or in other words, length along a line segment is the distance between its endpoints. This also proves that the d-dimensional Hausdorff measure scales by a factor of ‖r‖₊ ^ d when the set is scaled by r (both linearly and affinely), and that it is translation-invariant.

Estimated changes

Modified src/analysis/convex/between.lean

added theorem affine_segment_same

Modified src/measure_theory/measure/hausdorff.lean

added theorem measure_theory.hausdorff_measure_affine_segment

added theorem measure_theory.hausdorff_measure_homothety_image

added theorem measure_theory.hausdorff_measure_homothety_preimage

added theorem measure_theory.hausdorff_measure_line_map_image

added theorem measure_theory.hausdorff_measure_segment

added theorem measure_theory.hausdorff_measure_smul

added theorem measure_theory.hausdorff_measure_smul_right_image

added theorem measure_theory.measure.hausdorff_measure_smul₀

added theorem measure_theory.outer_measure.mk_metric_nnreal_smul

added theorem measure_theory.outer_measure.mk_metric_smul