Commit 2023-06-05 14:50 1b2a311a

View on Github →

feat: port MeasureTheory.Measure.Lebesgue.EqHaar (#4666)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Real/NNReal.lean

added theorem Real.toNNReal_ofNat

Created Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

added theorem AlternatingMap.measure_parallelepiped

added theorem Basis.parallelepiped_basisFun

added theorem MeasureTheory.Measure.NullMeasurableSet.const_smul

added theorem MeasureTheory.Measure.addHaar_parallelepiped

added theorem MeasureTheory.Measure.add_haar_affineSubspace

added theorem MeasureTheory.Measure.add_haar_ball

added theorem MeasureTheory.Measure.add_haar_ball_center

added theorem MeasureTheory.Measure.add_haar_ball_mul

added theorem MeasureTheory.Measure.add_haar_ball_mul_of_pos

added theorem MeasureTheory.Measure.add_haar_ball_of_pos

added theorem MeasureTheory.Measure.add_haar_closedBall'

added theorem MeasureTheory.Measure.add_haar_closedBall

added theorem MeasureTheory.Measure.add_haar_closedBall_center

added theorem MeasureTheory.Measure.add_haar_closedBall_eq_add_haar_ball

added theorem MeasureTheory.Measure.add_haar_closedBall_mul

added theorem MeasureTheory.Measure.add_haar_closedBall_mul_of_pos

added theorem MeasureTheory.Measure.add_haar_closed_unit_ball_eq_add_haar_unit_ball

added theorem MeasureTheory.Measure.add_haar_eq_zero_of_disjoint_translates

added theorem MeasureTheory.Measure.add_haar_eq_zero_of_disjoint_translates_aux

added theorem MeasureTheory.Measure.add_haar_image_continuousLinearEquiv

added theorem MeasureTheory.Measure.add_haar_image_continuousLinearMap

added theorem MeasureTheory.Measure.add_haar_image_homothety

added theorem MeasureTheory.Measure.add_haar_image_linearMap

added theorem MeasureTheory.Measure.add_haar_preimage_continuousLinearEquiv

added theorem MeasureTheory.Measure.add_haar_preimage_continuousLinearMap

added theorem MeasureTheory.Measure.add_haar_preimage_linearEquiv

added theorem MeasureTheory.Measure.add_haar_preimage_linearMap

added theorem MeasureTheory.Measure.add_haar_preimage_smul

added theorem MeasureTheory.Measure.add_haar_singleton_add_smul_div_singleton_add_smul

added theorem MeasureTheory.Measure.add_haar_smul

added theorem MeasureTheory.Measure.add_haar_smul_of_nonneg

added theorem MeasureTheory.Measure.add_haar_sphere

added theorem MeasureTheory.Measure.add_haar_sphere_of_ne_zero

added theorem MeasureTheory.Measure.add_haar_submodule

added theorem MeasureTheory.Measure.eventually_nonempty_inter_smul_of_density_one

added theorem MeasureTheory.Measure.map_add_haar_smul

added theorem MeasureTheory.Measure.map_linearMap_add_haar_eq_smul_add_haar

added theorem MeasureTheory.Measure.map_linearMap_add_haar_pi_eq_smul_add_haar

added theorem MeasureTheory.Measure.tendsto_add_haar_inter_smul_one_of_density_one

added theorem MeasureTheory.Measure.tendsto_add_haar_inter_smul_one_of_density_one_aux

added theorem MeasureTheory.Measure.tendsto_add_haar_inter_smul_zero_of_density_zero

added theorem MeasureTheory.Measure.tendsto_add_haar_inter_smul_zero_of_density_zero_aux1

added theorem MeasureTheory.Measure.tendsto_add_haar_inter_smul_zero_of_density_zero_aux2

added theorem MeasureTheory.addHaarMeasure_eq_volume

added theorem MeasureTheory.addHaarMeasure_eq_volume_pi

added def TopologicalSpace.PositiveCompacts.Icc01

added def TopologicalSpace.PositiveCompacts.piIcc01