Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-26 18:26 ef7fe6f9

View on Github →

feat(dynamics/ergodic/conservative): define conservative systems, formalize Poincaré recurrence thm (#2311)

Estimated changes

Modified src/combinatorics/pigeonhole.lean

added theorem nat.exists_lt_modeq_of_infinite

Modified src/data/set/finite.lean

added theorem set.infinite.exists_lt_map_eq_of_maps_to

added theorem set.infinite.exists_ne_map_eq_of_maps_to

Created src/dynamics/ergodic/conservative.lean

added theorem measure_theory.conservative.ae_forall_image_mem_imp_frequently_image_mem

added theorem measure_theory.conservative.ae_frequently_mem_of_mem_nhds

added theorem measure_theory.conservative.ae_mem_imp_frequently_image_mem

added theorem measure_theory.conservative.exists_gt_measure_inter_ne_zero

added theorem measure_theory.conservative.frequently_ae_mem_and_frequently_image_mem

added theorem measure_theory.conservative.frequently_measure_inter_ne_zero

added theorem measure_theory.conservative.inter_frequently_image_mem_ae_eq

added theorem measure_theory.conservative.measure_inter_frequently_image_mem_eq

added theorem measure_theory.conservative.measure_mem_forall_ge_image_not_mem_eq_zero

added structure measure_theory.conservative

Modified src/dynamics/ergodic/measure_preserving.lean

added theorem measure_theory.measure_preserving.exists_mem_image_mem

added theorem measure_theory.measure_preserving.exists_mem_image_mem_of_volume_lt_mul_volume

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.frequently_ae_iff

added theorem measure_theory.frequently_ae_mem_iff

added theorem measure_theory.measure_bUnion_null_iff

added theorem measure_theory.measure_diff_null'

added theorem measure_theory.measure_diff_null

Modified src/order/filter/basic.lean

added theorem filter.inter_eventually_eq_left

added theorem filter.inter_eventually_eq_right

Modified src/order/filter/cofinite.lean