Commit 2023-06-11 14:32 bd0681b8

View on Github →

feat: port MeasureTheory.Measure.Hausdorff (#4886)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/Hausdorff.lean

added theorem AntilipschitzWith.hausdorffMeasure_preimage_le

added theorem AntilipschitzWith.le_hausdorffMeasure_image

added theorem HolderOnWith.hausdorffMeasure_image_le

added theorem Isometry.hausdorffMeasure_image

added theorem Isometry.hausdorffMeasure_preimage

added theorem Isometry.map_hausdorffMeasure

added theorem IsometryEquiv.hausdorffMeasure_image

added theorem IsometryEquiv.hausdorffMeasure_preimage

added theorem IsometryEquiv.map_hausdorffMeasure

added theorem IsometryEquiv.measurePreserving_hausdorffMeasure

added theorem LipschitzOnWith.hausdorffMeasure_image_le

added theorem LipschitzWith.hausdorffMeasure_image_le

added def MeasureTheory.Measure.hausdorffMeasure

added theorem MeasureTheory.Measure.hausdorffMeasure_apply

added theorem MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum

added theorem MeasureTheory.Measure.hausdorffMeasure_le_liminf_tsum

added theorem MeasureTheory.Measure.hausdorffMeasure_le_one_of_subsingleton

added theorem MeasureTheory.Measure.hausdorffMeasure_mono

added theorem MeasureTheory.Measure.hausdorffMeasure_smul₀

added theorem MeasureTheory.Measure.hausdorffMeasure_zero_or_top

added theorem MeasureTheory.Measure.hausdorffMeasure_zero_singleton

added theorem MeasureTheory.Measure.le_hausdorffMeasure

added theorem MeasureTheory.Measure.le_mkMetric

added def MeasureTheory.Measure.mkMetric'

added theorem MeasureTheory.Measure.mkMetric'_toOuterMeasure

added def MeasureTheory.Measure.mkMetric

added theorem MeasureTheory.Measure.mkMetric_apply

added theorem MeasureTheory.Measure.mkMetric_le_liminf_sum

added theorem MeasureTheory.Measure.mkMetric_le_liminf_tsum

added theorem MeasureTheory.Measure.mkMetric_mono

added theorem MeasureTheory.Measure.mkMetric_mono_smul

added theorem MeasureTheory.Measure.mkMetric_toOuterMeasure

added theorem MeasureTheory.Measure.mkMetric_top

added theorem MeasureTheory.Measure.noAtoms_hausdorff

added theorem MeasureTheory.Measure.one_le_hausdorffMeasure_zero_of_nonempty

added theorem MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory

added theorem MeasureTheory.OuterMeasure.IsMetric.finset_iUnion_of_pairwise_separated

added theorem MeasureTheory.OuterMeasure.IsMetric.le_caratheodory

added def MeasureTheory.OuterMeasure.IsMetric

added theorem MeasureTheory.OuterMeasure.coe_mkMetric

added theorem MeasureTheory.OuterMeasure.isometryEquiv_comap_mkMetric

added theorem MeasureTheory.OuterMeasure.isometryEquiv_map_mkMetric

added theorem MeasureTheory.OuterMeasure.isometry_comap_mkMetric

added theorem MeasureTheory.OuterMeasure.isometry_map_mkMetric

added theorem MeasureTheory.OuterMeasure.le_mkMetric

added theorem MeasureTheory.OuterMeasure.mkMetric'.eq_iSup_nat

added theorem MeasureTheory.OuterMeasure.mkMetric'.le_pre

added theorem MeasureTheory.OuterMeasure.mkMetric'.mono_pre

added theorem MeasureTheory.OuterMeasure.mkMetric'.mono_pre_nat

added def MeasureTheory.OuterMeasure.mkMetric'.pre

added theorem MeasureTheory.OuterMeasure.mkMetric'.pre_le

added theorem MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre

added theorem MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre_nat

added theorem MeasureTheory.OuterMeasure.mkMetric'.trim_pre

added def MeasureTheory.OuterMeasure.mkMetric'

added theorem MeasureTheory.OuterMeasure.mkMetric'_isMetric

added def MeasureTheory.OuterMeasure.mkMetric

added theorem MeasureTheory.OuterMeasure.mkMetric_mono

added theorem MeasureTheory.OuterMeasure.mkMetric_mono_smul

added theorem MeasureTheory.OuterMeasure.mkMetric_nnreal_smul

added theorem MeasureTheory.OuterMeasure.mkMetric_smul

added theorem MeasureTheory.OuterMeasure.mkMetric_top

added theorem MeasureTheory.OuterMeasure.trim_mkMetric

added theorem MeasureTheory.hausdorffMeasure_affineSegment

added theorem MeasureTheory.hausdorffMeasure_homothety_image

added theorem MeasureTheory.hausdorffMeasure_homothety_preimage

added theorem MeasureTheory.hausdorffMeasure_lineMap_image

added theorem MeasureTheory.hausdorffMeasure_measurePreserving_funUnique

added theorem MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo

added theorem MeasureTheory.hausdorffMeasure_pi_real

added theorem MeasureTheory.hausdorffMeasure_prod_real

added theorem MeasureTheory.hausdorffMeasure_real

added theorem MeasureTheory.hausdorffMeasure_segment

added theorem MeasureTheory.hausdorffMeasure_smul

added theorem MeasureTheory.hausdorffMeasure_smul_right_image