Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-19 22:17 b4a2991c

View on Github →

feat(dynamics/ergodic): define measure preserving maps (#6764) Also prove some missing lemmas about measures.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.preimage_prod_map_prod

Created src/dynamics/ergodic/measure_preserving.lean

added theorem measure_theory.measure_preserving.comp

added theorem measure_theory.measure_preserving.measure_preimage

added theorem measure_theory.measure_preserving.prod

added theorem measure_theory.measure_preserving.skew_product

added structure measure_theory.measure_preserving

Modified src/measure_theory/giry_monad.lean

added theorem measure_theory.measure.bind_zero_left

added theorem measure_theory.measure.bind_zero_right'

added theorem measure_theory.measure.bind_zero_right

added theorem measure_theory.measure.join_zero

Modified src/measure_theory/measurable_space.lean

added theorem measurable.prod_map

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.ae_ne_bot

added theorem measure_theory.sigma_finite.of_map

Modified src/measure_theory/prod.lean

added theorem measure_theory.measure.map_prod_map

added theorem measure_theory.measure.prod_zero

added theorem measure_theory.measure.zero_prod