Ergodic maps / measures

Stream: Is there code for X?

[Oliver Nash]

I would like to be able to discuss ergodic maps (relative to a fixed measure). Looking now, it seems like we do not yet have the definition. Is this correct?

[Oliver Nash]

Assuming the above is correct, I would be grateful for any remarks on the following possible definitions:

import dynamics.ergodic.measure_preserving

open measure_theory measure_theory.measure

variables {α : Type*} [measurable_space α] (f : α → α)

set_option old_structure_cmd true

structure pre_ergodic (μ : measure α . volume_tac) : Prop :=
(measure_self_or_compl_eq_zero : ∀ s, measurable_set s → f ⁻¹' s = s → μ s = 0 ∨ μ sᶜ = 0)

structure ergodic (μ : measure α . volume_tac) extends
  measure_preserving f μ μ, pre_ergodic f μ

structure quasi_ergodic (μ : measure α . volume_tac) extends
  quasi_measure_preserving f μ μ, pre_ergodic f μ

[Johan Commelin]

In my mind @Yury G. Kudryashov is the local ergodic expert.

[Moritz Doll]

I am pretty sure that we don't have anything about ergodicity in Lean (I was looking at it when considering using Fourier series to prove (unique) ergodicity of circle maps - mainly as an application of the Fourier series).

[Oliver Nash]

I finally have a PR proposing the above: #17046