6.3. Basic API🔗

Mathlib contains basic structural API for working with ergodic maps. In some cases the weaker assumption of quasi-ergodicity is sufficient and in these cases the API is developed using this weaker assumption.

Examples of such API are:

• QuasiErgodic.ae_empty_or_univ₀: we may weaken strict invariance to almost invariance in the condition for a set to be almost empty or full.

• MeasureTheory.MeasurePreserving.preErgodic_conjugate_iff: ergodicity is preserved under conjugation with measure-preserving equivalences.

• Ergodic.ae_empty_or_univ_of_image_ae_le: for a finite measure space, a set whose image is almost contained in itself, must be almost empty or full.