Commit 2023-07-13 13:50 4b4b165a

View on Github →

chore(MeasureTheory): rename add_haar to addHaar (#5811) This is supposed to mean "an additive Haar measure", not adding something to Haar, so it should be one word and not two.

Estimated changes

Modified Mathlib/Analysis/Convex/Measure.lean

added theorem Convex.addHaar_frontier

deleted theorem Convex.add_haar_frontier

Modified Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

Modified Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean

Modified Mathlib/MeasureTheory/Integral/Periodic.lean

Modified Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean

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

added theorem MeasureTheory.Measure.addHaar_affineSubspace

added theorem MeasureTheory.Measure.addHaar_ball

added theorem MeasureTheory.Measure.addHaar_ball_center

added theorem MeasureTheory.Measure.addHaar_ball_mul

added theorem MeasureTheory.Measure.addHaar_ball_mul_of_pos

added theorem MeasureTheory.Measure.addHaar_ball_of_pos

added theorem MeasureTheory.Measure.addHaar_closedBall'

added theorem MeasureTheory.Measure.addHaar_closedBall

added theorem MeasureTheory.Measure.addHaar_closedBall_center

added theorem MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball

added theorem MeasureTheory.Measure.addHaar_closedBall_mul

added theorem MeasureTheory.Measure.addHaar_closedBall_mul_of_pos

added theorem MeasureTheory.Measure.addHaar_closed_unit_ball_eq_addHaar_unit_ball

added theorem MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates

added theorem MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates_aux

added theorem MeasureTheory.Measure.addHaar_image_continuousLinearEquiv

added theorem MeasureTheory.Measure.addHaar_image_continuousLinearMap

added theorem MeasureTheory.Measure.addHaar_image_homothety

added theorem MeasureTheory.Measure.addHaar_image_linearMap

added theorem MeasureTheory.Measure.addHaar_preimage_continuousLinearEquiv

added theorem MeasureTheory.Measure.addHaar_preimage_continuousLinearMap

added theorem MeasureTheory.Measure.addHaar_preimage_linearEquiv

added theorem MeasureTheory.Measure.addHaar_preimage_linearMap

added theorem MeasureTheory.Measure.addHaar_preimage_smul

added theorem MeasureTheory.Measure.addHaar_singleton_add_smul_div_singleton_add_smul

added theorem MeasureTheory.Measure.addHaar_smul

added theorem MeasureTheory.Measure.addHaar_smul_of_nonneg

added theorem MeasureTheory.Measure.addHaar_sphere

added theorem MeasureTheory.Measure.addHaar_sphere_of_ne_zero

added theorem MeasureTheory.Measure.addHaar_submodule

deleted theorem MeasureTheory.Measure.add_haar_affineSubspace

deleted theorem MeasureTheory.Measure.add_haar_ball

deleted theorem MeasureTheory.Measure.add_haar_ball_center

deleted theorem MeasureTheory.Measure.add_haar_ball_mul

deleted theorem MeasureTheory.Measure.add_haar_ball_mul_of_pos

deleted theorem MeasureTheory.Measure.add_haar_ball_of_pos

deleted theorem MeasureTheory.Measure.add_haar_closedBall'

deleted theorem MeasureTheory.Measure.add_haar_closedBall

deleted theorem MeasureTheory.Measure.add_haar_closedBall_center

deleted theorem MeasureTheory.Measure.add_haar_closedBall_eq_add_haar_ball

deleted theorem MeasureTheory.Measure.add_haar_closedBall_mul

deleted theorem MeasureTheory.Measure.add_haar_closedBall_mul_of_pos

deleted theorem MeasureTheory.Measure.add_haar_closed_unit_ball_eq_add_haar_unit_ball

deleted theorem MeasureTheory.Measure.add_haar_eq_zero_of_disjoint_translates

deleted theorem MeasureTheory.Measure.add_haar_eq_zero_of_disjoint_translates_aux

deleted theorem MeasureTheory.Measure.add_haar_image_continuousLinearEquiv

deleted theorem MeasureTheory.Measure.add_haar_image_continuousLinearMap

deleted theorem MeasureTheory.Measure.add_haar_image_homothety

deleted theorem MeasureTheory.Measure.add_haar_image_linearMap

deleted theorem MeasureTheory.Measure.add_haar_preimage_continuousLinearEquiv

deleted theorem MeasureTheory.Measure.add_haar_preimage_continuousLinearMap

deleted theorem MeasureTheory.Measure.add_haar_preimage_linearEquiv

deleted theorem MeasureTheory.Measure.add_haar_preimage_linearMap

deleted theorem MeasureTheory.Measure.add_haar_preimage_smul

deleted theorem MeasureTheory.Measure.add_haar_singleton_add_smul_div_singleton_add_smul

deleted theorem MeasureTheory.Measure.add_haar_smul

deleted theorem MeasureTheory.Measure.add_haar_smul_of_nonneg

deleted theorem MeasureTheory.Measure.add_haar_sphere

deleted theorem MeasureTheory.Measure.add_haar_sphere_of_ne_zero

deleted theorem MeasureTheory.Measure.add_haar_submodule

added theorem MeasureTheory.Measure.map_addHaar_smul

deleted theorem MeasureTheory.Measure.map_add_haar_smul

added theorem MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar

added theorem MeasureTheory.Measure.map_linearMap_addHaar_pi_eq_smul_addHaar

deleted theorem MeasureTheory.Measure.map_linearMap_add_haar_eq_smul_add_haar

deleted theorem MeasureTheory.Measure.map_linearMap_add_haar_pi_eq_smul_add_haar

added theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one

added theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one_aux

added theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero

added theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero_aux1

added theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero_aux2

deleted theorem MeasureTheory.Measure.tendsto_add_haar_inter_smul_one_of_density_one

deleted theorem MeasureTheory.Measure.tendsto_add_haar_inter_smul_one_of_density_one_aux

deleted theorem MeasureTheory.Measure.tendsto_add_haar_inter_smul_zero_of_density_zero

deleted theorem MeasureTheory.Measure.tendsto_add_haar_inter_smul_zero_of_density_zero_aux1

deleted theorem MeasureTheory.Measure.tendsto_add_haar_inter_smul_zero_of_density_zero_aux2