Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-24 12:56 79887c96

View on Github →

feat(measure_theory/group/prod): generalize topological groups to measurable groups (#11933)

This fixes the gap in [Halmos] that I mentioned in measure_theory.group.prod
Thanks to @sgouezel for giving me the proof to fill that gap.
A text proof to fill the gap is here

Estimated changes

Modified src/algebra/indicator_function.lean

added theorem set.mul_indicator_image

Modified src/measure_theory/group/measure.lean

Modified src/measure_theory/group/prod.lean

added theorem measure_theory.absolutely_continuous_of_is_mul_left_invariant

added theorem measure_theory.ae_measure_preimage_mul_right_lt_top

added theorem measure_theory.ae_measure_preimage_mul_right_lt_top_of_ne_zero

added theorem measure_theory.measure_eq_div_smul

modified theorem measure_theory.measure_lintegral_div_measure

added theorem measure_theory.measure_mul_lintegral_eq

modified theorem measure_theory.measure_mul_measure_eq

Modified src/measure_theory/measure/haar.lean

Modified src/measure_theory/measure/measure_space.lean

added theorem measurable_equiv.sigma_finite_map

added theorem measure_theory.ae_of_forall_measure_lt_top_ae_restrict'