Commit 2023-05-30 10:47 e2aa8015

View on Github →

feat: port MeasureTheory.Group.Measure (#4496)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Group/Measure.lean

added theorem MeasureTheory.Measure.HaarMeasure.smul

added theorem MeasureTheory.Measure.haarMeasure_map

added theorem MeasureTheory.Measure.haarMeasure_of_isCompact_nonempty_interior

added theorem MeasureTheory.Measure.haar_singleton

added theorem MeasureTheory.Measure.inv_apply

added theorem MeasureTheory.Measure.inv_eq_self

added theorem MeasureTheory.Measure.map_div_left_ae

added theorem MeasureTheory.Measure.map_div_left_eq_self

added theorem MeasureTheory.Measure.map_inv_eq_self

added theorem MeasureTheory.Measure.map_mul_right_inv_eq_self

added theorem MeasureTheory.Measure.measurePreserving_div_left

added theorem MeasureTheory.Measure.measurePreserving_inv

added theorem MeasureTheory.Measure.measurePreserving_mul_right_inv

added theorem MeasureTheory.Measure.measure_inv

added theorem MeasureTheory.Measure.measure_preimage_inv

added theorem MeasureTheory.MeasurePreserving.mul_left

added theorem MeasureTheory.MeasurePreserving.mul_right

added theorem MeasureTheory.eventually_div_right_iff

added theorem MeasureTheory.eventually_mul_left_iff

added theorem MeasureTheory.eventually_mul_right_iff

added theorem MeasureTheory.forall_measure_preimage_mul_iff

added theorem MeasureTheory.forall_measure_preimage_mul_right_iff

added theorem MeasureTheory.map_div_right_ae

added theorem MeasureTheory.map_div_right_eq_self

added theorem MeasureTheory.map_mul_left_ae

added theorem MeasureTheory.map_mul_left_eq_self

added theorem MeasureTheory.map_mul_right_ae

added theorem MeasureTheory.map_mul_right_eq_self

added theorem MeasureTheory.measurePreserving_div_right

added theorem MeasureTheory.measurePreserving_mul_left

added theorem MeasureTheory.measurePreserving_mul_right

added theorem MeasureTheory.measure_lt_top_of_isCompact_of_mulLeftInvariant'

added theorem MeasureTheory.measure_lt_top_of_isCompact_of_mulLeftInvariant

added theorem MeasureTheory.measure_ne_zero_iff_nonempty_of_mulLeftInvariant

added theorem MeasureTheory.measure_pos_iff_nonempty_of_mulLeftInvariant

added theorem MeasureTheory.measure_preimage_mul

added theorem MeasureTheory.measure_preimage_mul_right

added theorem MeasureTheory.measure_univ_of_mulLeftInvariant

added theorem MeasureTheory.mulLeftInvariant_map

added theorem MeasureTheory.null_iff_of_mulLeftInvariant

added theorem MeasureTheory.openPosMeasure_of_mulLeftInvariant_of_compact

added theorem MeasureTheory.openPosMeasure_of_mulLeftInvariant_of_regular

added theorem MeasureTheory.regular_inv_iff