Commit 2024-07-25 09:16 e0e1733a

View on Github →

feat(Ergodic/Conservative): generalize to NullMeasurableSets (#15086)

add IsOpen.nullMeasurableSet and IsClosed.nullMeasurableSet;
add ' to the name of the field of Conservative;
add non-primed version that works for NullMeasurableSets;
generalize other theorems in Ergodic/Conservative to NullMeasurableSets.

Estimated changes

Modified Mathlib/Dynamics/Ergodic/Conservative.lean

modified theorem MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem

modified theorem MeasureTheory.Conservative.exists_gt_measure_inter_ne_zero

added theorem MeasureTheory.Conservative.exists_mem_iterate_mem

modified theorem MeasureTheory.Conservative.frequently_ae_mem_and_frequently_image_mem

modified theorem MeasureTheory.Conservative.frequently_measure_inter_ne_zero

modified theorem MeasureTheory.Conservative.inter_frequently_image_mem_ae_eq

modified theorem MeasureTheory.Conservative.measure_inter_frequently_image_mem_eq

modified theorem MeasureTheory.Conservative.measure_mem_forall_ge_image_not_mem_eq_zero

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

added theorem IsClosed.nullMeasurableSet

added theorem IsOpen.nullMeasurableSet