Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-24 02:33 f578d1d6

View on Github →

feat(measure_theory): TC for smul-invariant measures (#10325)

Estimated changes

Modified src/dynamics/ergodic/measure_preserving.lean

added theorem measure_theory.measure_preserving.measure_preimage_emb

Created src/measure_theory/group/action.lean

added theorem measure_theory.is_locally_finite_measure_of_smul_invariant

added theorem measure_theory.map_smul

added theorem measure_theory.measure_eq_zero_iff_eq_empty_of_smul_invariant

added theorem measure_theory.measure_is_open_pos_of_smul_invariant_of_compact_ne_zero

added theorem measure_theory.measure_is_open_pos_of_smul_invariant_of_ne_zero

added theorem measure_theory.measure_pos_iff_nonempty_of_smul_invariant

added theorem measure_theory.measure_preimage_smul

added theorem measure_theory.measure_preserving_smul

added theorem measure_theory.measure_smul_set

added theorem measure_theory.smul_invariant_measure_tfae

Created src/measure_theory/group/fundamental_domain.lean

added structure measure_theory.is_add_fundamental_domain

added theorem measure_theory.is_fundamental_domain.Union_smul_ae_eq

added theorem measure_theory.is_fundamental_domain.measurable_set_smul

added theorem measure_theory.is_fundamental_domain.measure_eq_tsum'

added theorem measure_theory.is_fundamental_domain.measure_eq_tsum

added theorem measure_theory.is_fundamental_domain.pairwise_ae_disjoint

added structure measure_theory.is_fundamental_domain

Modified src/measure_theory/integral/lebesgue.lean

Modified src/measure_theory/measure/measure_space_def.lean

modified theorem measure_theory.measure_Union_null_iff

added theorem measure_theory.measure_sUnion_null_iff