Commit 2023-05-22 19:15 d4dbf928

View on Github →

feat: port Dynamics.Ergodic.Conservative (#4230)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/Ergodic/Conservative.lean

added theorem MeasureTheory.Conservative.ae_forall_image_mem_imp_frequently_image_mem

added theorem MeasureTheory.Conservative.ae_frequently_mem_of_mem_nhds

added theorem MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem

added theorem MeasureTheory.Conservative.exists_gt_measure_inter_ne_zero

added theorem MeasureTheory.Conservative.frequently_ae_mem_and_frequently_image_mem

added theorem MeasureTheory.Conservative.frequently_measure_inter_ne_zero

added theorem MeasureTheory.Conservative.inter_frequently_image_mem_ae_eq

added theorem MeasureTheory.Conservative.measure_inter_frequently_image_mem_eq

added theorem MeasureTheory.Conservative.measure_mem_forall_ge_image_not_mem_eq_zero

added structure MeasureTheory.Conservative