Groups with dense roots

Stream: maths

[Yury G. Kudryashov]

Is there a nicer description (or a nicer sufficient condition) for compact topological groups with the following properties?

• x ↦ x^n is surjective for n > 0 (I know about docs#RootableBy)
• for all n > 1, the set ⋃ k, {x | x^{n^k} = 1} is dense

#xy: These are sufficient conditions for x ↦ x^n, n > 1, to be ergodic, generalizing docs#AddCircle.ergodic_nsmul formalized by @Oliver Nash, see MonoidHom.ergodic_of_dense_iUnion_preimage_one in #16577

[Oliver Nash]

Neat! I have a pretty full day tomorrow but I will have some time to catch up with my review in the evening so I'll look closely then.

[Oliver Nash]

There's actually a related lemma I've been meaning to generalise for 18 months or something. Namely: docs#AddCircle.ae_empty_or_univ_of_forall_vadd_ae_eq_self

[Oliver Nash]

The assumption hu₁ : ∀ i, (u i +ᵥ s : Set _) =ᵐ[volume] s is stronger than necessary. One can allow some positive measure for the symmetric difference between u i +ᵥ s and s as long as the measure of this discrepancy tends to zero along quadratically wrt addOrderOf ∘ u.

(I pestered Sébastien about this in Leiden and he showed me a proof and I've felt guilty ever since that I haven't formalised it.)

[Yury G. Kudryashov]

For the original (non-generalized) lemma, another proof is: the subgroup generated by these u i is dense, hence aeconst_of_dense_setOf_preimage_vadd_ae from my PR applies.

[Yury G. Kudryashov]

I think that the generalized lemma can be proved using my machinery too. I'll double check tonight, then post more details.

[Yury G. Kudryashov]

Here is the proof (in multiplicative notation):

• Due to docs#MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero, μ (((g • ·) ⁻¹' s) ∆ s) is continuous in g.
• Thus it suffices to show that {g | μ (((g • ·) ⁻¹' s) ∆ s) < ε} is dense for all ε > 0.
• Now assume that there exists a sequence g n such that orderOf (g n) → ∞ and orderOf (g n) * μ (((g n • ·) ⁻¹' s) ∆ s) → 0 as n → ∞.
• Take ε > 0 and a nonempty open set U.
• Take n such that orderOf (g n) * μ (((g n • ·) ⁻¹' s) ∆ s) < ε, then take k < orderOf (g n) such that (g n) ^ k ∈ U.
• By triangle inequality, μ ((((g n) ^ k • ·) ⁻¹' s) ∆ s) ≤ orderOf (g n) * μ (((g n • ·) ⁻¹' s) ∆ s) < ε. q.e.d.

[Yury G. Kudryashov]

Note that the assumption orderOf (g n) * μ (((g n • ·) ⁻¹' s) ∆ s) → 0 is weaker than "tends to zero quadratically".

[Yury G. Kudryashov]

BTW, ergodicity of an irrational rotation is formalized in #16603 (needs a lot of polishing before marking as ready for review).