ergodic group actions

Stream: maths

[Yury G. Kudryashov]

Am I right that we have ergodic function but we don't have ergodic actions? Tagging his majesty @Oliver Nash , the author of file#Dynamics/Ergodic/Ergodic

[Yury G. Kudryashov]

Also, what's the right definition:

  ∀ s, MeasurableSet s → (∀ g, (g • ·) ⁻¹' s =ᵐ[μ] s) → (s =ᵐ[μ] (∅ : Set α) ∨ s =ᵐ[μ] univ)

or

  ∀ s, MeasurableSet s → (∀ g, (g • ·) ⁻¹' s = s) → (s =ᵐ[μ] (∅ : Set α) ∨ s =ᵐ[μ] univ)

For a single map these are equivalent due to docs#MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae but for an uncountable group, I'm not sure (I ignored this difference up until today).

[Yury G. Kudryashov]

@Sébastien Gouëzel :up:

[Oliver Nash]

We do not have ergodic group actions.

[Oliver Nash]

Also, I believe the "right" definition is the first one which requires (g • ·) ⁻¹' s =ᵐ[μ] s rather than strict equality. Moreover I would advocate changing docs#PreErgodic to require this stronger hypothesis.

[Oliver Nash]

Oh one other thing, if we do change docs#PreErgodic then for (quasi-) measure-preserving maps, I think we should provide an alternate constructor demanding only the property for strictly invariant sets.

[Oliver Nash]

And likewise for the group action case: there should be an alternate constructor demanding a proof only for strictly-invariant sets when the action is qmp and the group is sufficiently well-behaved (e.g., countable, but presumably there are much weaker hypotheses).

[Oliver Nash]

I should emphasise that I barely know anything about ergodicity though, so let's wait for an expert, hopefully Sebastien :-)

[Yaël Dillies]

I think I discussed this in PM with @Yury G. Kudryashov, who argued that the current definition was best? I disagreed at the time though

[Yury G. Kudryashov]

For a single quasi measure preserving map, these definitions are equivalent. I don't know if people use docs#PreErgodic.

[Yury G. Kudryashov]

@Yaël Dillies I went through our DM history and found no traces of this discussion.

[Yaël Dillies]

Hmm, maybe it was with Sébastien instead

[Felix Weilacher]

Yury G. Kudryashov said:

For a single quasi measure preserving map, these definitions are equivalent. I don't know if people use docs#PreErgodic.

I have not worked with ergodicity in lean, but in my circles "Ergodic" means docs#PreErgodic

[Felix Weilacher]

I am also confused by some of the above discussion. For a countable group the two definitions are equivalent whether or not your action is quasi mp.

[Felix Weilacher]

I've never seen "ergodic" used for uncountable group actions so I guess I'm not completely sure about the original question. I have advocated before for defining ergodicity in terms of equivalence relations rather than group actions, and taking this perspective probably supports the second definition.

[Felix Weilacher]

A litmus test could be: Should transitive actions be ergodic? Because there are transitive actions of uncountable groups that fail the first definition.

[Sébastien Gouëzel]

Measure-preserving actions of uncountable groups are definitely important (Lie group actions, for instance, but not only). I have just checked one of the standard references on advanced ergodic theory (Aaronson's "An introduction to infinite ergodic theory") and he defines ergodic actions of uncountable groups as follows: if a measurable set A satisfies gA =[\mu] A for all g, then \mu A = 0 or \mu A^c = 0.

[Yury G. Kudryashov]

So, they use the first definition.

[Yury G. Kudryashov]

BTW, I have a PR (#14596 with dependencies) proving that the left action is ergodic in this sense. Next in line: use it and #14500 to prove that a set invariant under a dense set of left shifts is null or a.e. all.

[Yury G. Kudryashov]

One more question: should we care about monoid actions in this context?

[Yury G. Kudryashov]

#14952 defines ergodic monoid/group actions. It depends on #14891 which defines IterateMulAct wrapper that helps relate our MulAction typeclasses to predicates about functions.