Commit 2026-09-18 11:47 86952bd6

feat(Dynamics/Ergodic): stronger PreErgodic definition (#43484) This PR changes the PreErgodic definition to quantify over almost-invariant null measurable sets instead of strictly invariant measurable sets. It makes the definition invariant with respect to almost-everywhere equality of maps, which was not the case before. The initial motivation for this change is as prior work for making MeasurePreserving assume the map f is AEMeasurable instead of Measurable. With that change, the previous definition in terms of strictly invariant measurable sets cannot be proven from the almost-everywhere version (previously QuasiErgodic.ae_empty_or_univ), and would instead require an additional measurability hypothesis for f.

[1]: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/PreErgodic.20definition/with/620793508