Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-29 03:47 fc4e471b

View on Github →

feat(measure_theory/group/basic): make is_[add|mul]_[left|right]_invariant classes (#11655)

Simplify the definitions of these classes
Generalize many results about topological groups to measurable groups (still to do in group/prod)
Simplify some proofs
Make function argument of integral_mul_[left|right]_eq_self explicit (otherwise it is hard to apply this lemma in case the function is not a variable)

Estimated changes

Modified src/analysis/fourier.lean

Modified src/measure_theory/group/basic.lean

added theorem measure_theory.forall_measure_preimage_mul_iff

added theorem measure_theory.forall_measure_preimage_mul_right_iff

deleted theorem measure_theory.is_mul_left_invariant.inv

deleted theorem measure_theory.is_mul_left_invariant.measure_lt_top_of_is_compact'

deleted theorem measure_theory.is_mul_left_invariant.measure_lt_top_of_is_compact

deleted theorem measure_theory.is_mul_left_invariant.measure_ne_zero_iff_nonempty

deleted theorem measure_theory.is_mul_left_invariant.measure_pos_iff_nonempty

deleted theorem measure_theory.is_mul_left_invariant.measure_pos_of_is_open

deleted theorem measure_theory.is_mul_left_invariant.measure_preimage_mul

deleted theorem measure_theory.is_mul_left_invariant.null_iff

deleted theorem measure_theory.is_mul_left_invariant.null_iff_empty

deleted theorem measure_theory.is_mul_left_invariant.smul

deleted def measure_theory.is_mul_left_invariant

deleted theorem measure_theory.is_mul_left_invariant_inv

deleted theorem measure_theory.is_mul_right_invariant.inv

deleted theorem measure_theory.is_mul_right_invariant.smul

deleted def measure_theory.is_mul_right_invariant

deleted theorem measure_theory.is_mul_right_invariant_inv

modified theorem measure_theory.lintegral_eq_zero_of_is_mul_left_invariant

modified theorem measure_theory.lintegral_mul_left_eq_self

modified theorem measure_theory.lintegral_mul_right_eq_self

added theorem measure_theory.map_mul_left_eq_self

added theorem measure_theory.map_mul_right_eq_self

deleted theorem measure_theory.measure.haar_preimage_mul

deleted theorem measure_theory.measure.haar_preimage_mul_right

modified theorem measure_theory.measure.inv_apply

deleted theorem measure_theory.measure.is_mul_left_invariant_haar

deleted theorem measure_theory.measure.map_mul_left_eq_self

deleted theorem measure_theory.measure.map_mul_right_eq_self

added theorem measure_theory.measure_lt_top_of_is_compact_of_is_mul_left_invariant'

added theorem measure_theory.measure_lt_top_of_is_compact_of_is_mul_left_invariant

added theorem measure_theory.measure_ne_zero_iff_nonempty_of_is_mul_left_invariant

added theorem measure_theory.measure_pos_iff_nonempty_of_is_mul_left_invariant

added theorem measure_theory.measure_pos_of_is_open_of_is_mul_left_invariant

added theorem measure_theory.measure_preimage_mul

added theorem measure_theory.measure_preimage_mul_right

added theorem measure_theory.null_iff_empty_of_is_mul_left_invariant

added theorem measure_theory.null_iff_of_is_mul_left_invariant

modified theorem measure_theory.regular_inv_iff

Modified src/measure_theory/group/prod.lean

modified theorem measure_theory.lintegral_lintegral_mul_inv

modified theorem measure_theory.map_prod_inv_mul_eq

modified theorem measure_theory.map_prod_inv_mul_eq_swap

modified theorem measure_theory.map_prod_mul_eq

modified theorem measure_theory.map_prod_mul_eq_swap

modified theorem measure_theory.map_prod_mul_inv_eq

modified theorem measure_theory.measure_inv_null

modified theorem measure_theory.measure_lintegral_div_measure

modified theorem measure_theory.measure_mul_measure_eq

modified theorem measure_theory.measure_mul_right_ne_zero

modified theorem measure_theory.measure_mul_right_null

modified theorem measure_theory.quasi_measure_preserving_inv

Modified src/measure_theory/integral/bochner.lean

modified theorem measure_theory.integral_mul_left_eq_self

modified theorem measure_theory.integral_mul_right_eq_self

modified theorem measure_theory.integral_zero_of_mul_left_eq_neg

modified theorem measure_theory.integral_zero_of_mul_right_eq_neg

Modified src/measure_theory/measure/haar.lean

modified theorem measure_theory.measure.haar_measure_unique

deleted theorem measure_theory.measure.is_mul_left_invariant_haar_measure

modified theorem measure_theory.measure.regular_of_is_mul_left_invariant

Modified src/measure_theory/measure/haar_lebesgue.lean

deleted theorem measure_theory.is_add_left_invariant_real_volume

deleted theorem measure_theory.is_add_left_invariant_real_volume_pi