Ergodicity from minimality

In this file we prove that the left shift (a * ·) on a compact topological group G is ergodic with respect to the Haar measure if and only if it is minimal, i.e., the powers a ^ n are dense in G.

The proof of the more difficult "if minimal, then ergodic" implication is based on the ergodicity of the left action of a group on itself and the following fact that we prove in ergodic_smul_of_denseRange_pow below:

If a monoid M continuously acts on an R₁ topological space X, g is an element of M such that its natural powers are dense in M, and μis a finite inner regular measure onXwhich is ergodic with respect to the action ofM, then the scalar multiplication by g` is an ergodic map.

We also prove that a continuous monoid homomorphism f : G →* G is ergodic, if it is surjective and the preimages of 1 under iterations of f are dense in the group. This theorem applies, e.g., to the map z ↦ n • z on the additive circle or a torus.

theorem aeconst_of_dense_setOf_preimage_smul_ae {M : Type u_1} [TopologicalSpace M] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [SMul M X] [ContinuousSMul M X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense {g : M | (fun (x : X) => g • x) ⁻¹' s =ᵐ[μ] s}) : Filter.EventuallyConst s (MeasureTheory.ae μ)

Let M act continuously on an R₁ topological space X. Let μ be a finite inner regular measure on X which is ergodic with respect to this action. If a null measurable set s is a.e. equal to its preimages under the action of a dense set of elements of M, then it is either null or conull.

theorem aeconst_of_dense_setOf_preimage_vadd_ae {M : Type u_1} [TopologicalSpace M] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [VAdd M X] [ContinuousVAdd M X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense {g : M | (fun (x : X) => g +ᵥ x) ⁻¹' s =ᵐ[μ] s}) : Filter.EventuallyConst s (MeasureTheory.ae μ)

Let M act continuously on an R₁ topological space X. Let μ be a finite inner regular measure on X which is ergodic with respect to this action. If a null measurable set s is a.e. equal to its preimages under the action of a dense set of elements of M, then it is either null or conull.

theorem aeconst_of_dense_setOf_preimage_smul_eq {M : Type u_1} [TopologicalSpace M] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [SMul M X] [ContinuousSMul M X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense {g : M | (fun (x : X) => g • x) ⁻¹' s = s}) : Filter.EventuallyConst s (MeasureTheory.ae μ)

theorem aeconst_of_dense_setOf_preimage_vadd_eq {M : Type u_1} [TopologicalSpace M] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [VAdd M X] [ContinuousVAdd M X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense {g : M | (fun (x : X) => g +ᵥ x) ⁻¹' s = s}) : Filter.EventuallyConst s (MeasureTheory.ae μ)

theorem ergodic_smul_of_denseRange_pow {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] {M : Type u_3} [Monoid M] [TopologicalSpace M] [MulAction M X] [ContinuousSMul M X] {g : M} (hg : DenseRange fun (x : ℕ) => g ^ x) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] : Ergodic (fun (x : X) => g • x) μ

If a monoid M continuously acts on an R₁ topological space X, g is an element of M such that its natural powers are dense in M, and μis a finite inner regular measure onXwhich is ergodic with respect to the action ofM, then the scalar multiplication by g` is an ergodic map.

theorem ergodic_vadd_of_denseRange_nsmul {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] {M : Type u_3} [AddMonoid M] [TopologicalSpace M] [AddAction M X] [ContinuousVAdd M X] {g : M} (hg : DenseRange fun (x : ℕ) => x • g) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ] : Ergodic (fun (x : X) => g +ᵥ x) μ

If an additive monoid M continuously acts on an R₁ topological space X, g is an element of M such that its natural multiples are dense in M, and μis a finite inner regular measure onXwhich is ergodic with respect to the action ofM, then the vector addition of g` is an ergodic map.

theorem ErgodicSMul.trans_isMinimal {M : Type u_1} {X : Type u_2} [Monoid M] [SMul M X] [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] (N : Type u_3) [MulAction M N] [Monoid N] [TopologicalSpace N] [MulAction.IsMinimal M N] [MulAction N X] [IsScalarTower M N X] [ContinuousSMul N X] [ErgodicSMul N X μ] : ErgodicSMul M X μ

If N acts continuously and ergodically on X and M acts minimally on N, then the corresponding action of M on X is ergodic.

theorem ErgodicVAdd.trans_isMinimal {M : Type u_1} {X : Type u_2} [AddMonoid M] [VAdd M X] [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] (N : Type u_3) [AddAction M N] [AddMonoid N] [TopologicalSpace N] [AddAction.IsMinimal M N] [AddAction N X] [VAddAssocClass M N X] [ContinuousVAdd N X] [ErgodicVAdd N X μ] : ErgodicVAdd M X μ

If N acts additively continuously and ergodically on X and M acts minimally on N, then the corresponding action of M on X is ergodic.

theorem aeconst_of_dense_aestabilizer_smul {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousInv G] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [MulAction G X] [ContinuousSMul G X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul G X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense ↑(MulAction.aestabilizer G μ s)) : Filter.EventuallyConst s (MeasureTheory.ae μ)

theorem aeconst_of_dense_aestabilizer_vadd {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousNeg G] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [AddAction G X] [ContinuousVAdd G X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd G X μ] {s : Set X} (hsm : MeasureTheory.NullMeasurableSet s μ) (hd : Dense ↑(AddAction.aestabilizer G μ s)) : Filter.EventuallyConst s (MeasureTheory.ae μ)

theorem ergodic_smul_of_denseRange_zpow {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousInv G] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [MulAction G X] [ContinuousSMul G X] {g : G} (hg : DenseRange fun (x : ℤ) => g ^ x) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul G X μ] : Ergodic (fun (x : X) => g • x) μ

If a monoid M continuously acts on an R₁ topological space X, g is an element of M such that its integer powers are dense in M, and μis a finite inner regular measure onXwhich is ergodic with respect to the action ofM, then the scalar multiplication by g` is an ergodic map.

theorem ergodic_vadd_of_denseRange_zsmul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousNeg G] {X : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X] [BorelSpace X] [AddAction G X] [ContinuousVAdd G X] {g : G} (hg : DenseRange fun (x : ℤ) => x • g) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd G X μ] : Ergodic (fun (x : X) => g +ᵥ x) μ

If an additive monoid M continuously acts on an R₁ topological space X, g is an element of M such that its integer multiples are dense in M, and μis a finite inner regular measure onXwhich is ergodic with respect to the action ofM, then the vector addition of g` is an ergodic map.

theorem DenseRange.zpow_of_ergodic_mul_left {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [MeasurableSpace G] [OpensMeasurableSpace G] {μ : MeasureTheory.Measure G} [μ.IsOpenPosMeasure] {g : G} (hg : Ergodic (fun (x : G) => g * x) μ) : DenseRange fun (x : ℤ) => g ^ x

If the left multiplication by g is ergodic with respect to a measure which is positive on nonempty open sets, then the integer powers of g are dense in G.

theorem DenseRange.zsmul_of_ergodic_add_left {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [MeasurableSpace G] [OpensMeasurableSpace G] {μ : MeasureTheory.Measure G} [μ.IsOpenPosMeasure] {g : G} (hg : Ergodic (fun (x : G) => g + x) μ) : DenseRange fun (x : ℤ) => x • g

If the left addition of g is ergodic with respect to a measure which is positive on nonempty open sets, then the integer multiples of g are dense in G.

theorem ergodic_mul_left_of_denseRange_pow {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [MeasurableSpace G] [SecondCountableTopology G] [BorelSpace G] {g : G} (hg : DenseRange fun (x : ℕ) => g ^ x) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsMulLeftInvariant] : Ergodic (fun (x : G) => g * x) μ

theorem ergodic_add_left_of_denseRange_nsmul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [MeasurableSpace G] [SecondCountableTopology G] [BorelSpace G] {g : G} (hg : DenseRange fun (x : ℕ) => x • g) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsAddLeftInvariant] : Ergodic (fun (x : G) => g + x) μ

theorem ergodic_mul_left_of_denseRange_zpow {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [MeasurableSpace G] [SecondCountableTopology G] [BorelSpace G] {g : G} (hg : DenseRange fun (x : ℤ) => g ^ x) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsMulLeftInvariant] : Ergodic (fun (x : G) => g * x) μ

theorem ergodic_add_left_of_denseRange_zsmul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [MeasurableSpace G] [SecondCountableTopology G] [BorelSpace G] {g : G} (hg : DenseRange fun (x : ℤ) => x • g) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsAddLeftInvariant] : Ergodic (fun (x : G) => g + x) μ

theorem ergodic_mul_left_iff_denseRange_zpow {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [MeasurableSpace G] [SecondCountableTopology G] [BorelSpace G] {g : G} (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsMulLeftInvariant] [NeZero μ] : Ergodic (fun (x : G) => g * x) μ ↔ DenseRange fun (x : ℤ) => g ^ x

theorem ergodic_add_left_iff_denseRange_zsmul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [MeasurableSpace G] [SecondCountableTopology G] [BorelSpace G] {g : G} (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsAddLeftInvariant] [NeZero μ] : Ergodic (fun (x : G) => g + x) μ ↔ DenseRange fun (x : ℤ) => x • g

theorem MonoidHom.preErgodic_of_dense_iUnion_preimage_one {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [SecondCountableTopology G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsMulLeftInvariant] (f : G →* G) (hf : Dense (⋃ (n : ℕ), (⇑f)^[n] ⁻¹' 1)) : PreErgodic (⇑f) μ

Let f : G →* G be a group endomorphism of a topological group with second countable topology. If the preimages of 1 under the iterations of f are dense, then it is preergodic with respect to any finite inner regular left invariant measure.

theorem AddMonoidHom.preErgodic_of_dense_iUnion_preimage_zero {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [SecondCountableTopology G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsAddLeftInvariant] (f : G →+ G) (hf : Dense (⋃ (n : ℕ), (⇑f)^[n] ⁻¹' 0)) : PreErgodic (⇑f) μ

Let f : G →+ G be an additive group endomorphism of a topological additive group with second countable topology. If the preimages of 0 under the iterations of f are dense, then it is preergodic with respect to any finite inner regular left invariant measure.

theorem MonoidHom.ergodic_of_dense_iUnion_preimage_one {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [SecondCountableTopology G] [MeasurableSpace G] [BorelSpace G] [CompactSpace G] {μ : MeasureTheory.Measure G} [μ.IsHaarMeasure] (f : G →* G) (hf : Dense (⋃ (n : ℕ), (⇑f)^[n] ⁻¹' 1)) (hcont : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Ergodic (⇑f) μ

Let f : G →* G be a continuous surjective group endomorphism of a compact topological group with second countable topology. If the preimages of 1 under the iterations of f are dense, then f is ergodic with respect to any finite inner regular left invariant measure.

theorem AddMonoidHom.ergodic_of_dense_iUnion_preimage_zero {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [SecondCountableTopology G] [MeasurableSpace G] [BorelSpace G] [CompactSpace G] {μ : MeasureTheory.Measure G} [μ.IsAddHaarMeasure] (f : G →+ G) (hf : Dense (⋃ (n : ℕ), (⇑f)^[n] ⁻¹' 0)) (hcont : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Ergodic (⇑f) μ

Let f : G →+ G be a continuous surjective additive group endomorphism of a compact topological additive group with second countable topology. If the preimages of 0 under the iterations of f are dense, then f is ergodic with respect to any finite inner regular left invariant measure.