Halmos's generic weak-mixing theorem

halmos_generic_weak_mixing

Submitter: Kim Morrison.

Notes: On a non-atomic standard probability space (X, m), the set of weakly mixing measure-preserving automorphisms contains a dense Gδ in the weak topology on the automorphism group, AND every weakly mixing automorphism is ergodic. The Lean statement is the conjunction of these two claims: the genericity (existence of a Gδ-dense subset of weakly mixing automorphisms) and the global implication (weakly mixing ⇒ ergodic for every automorphism). The weak topology on `Automorphism m` is the topology generated by neighbourhoods `{T | m((T '' A) ∆ (T₀ '' A)) < ε}` over base points T₀, measurable A, and ε > 0; this matches Knill's `T_j → T` iff `m(T_j(A) ∆ T(A)) → 0` for every measurable A. Weak mixing is the Cesàro decay `|m((T^k)⁻¹ A ∩ B) − m A · m B|` → 0. The [NoAtoms m] hypothesis is essential. For example, on `Bool` with equal atom masses the automorphism group is finite, the weak topology is discrete, and dense would force G = univ, but the identity is not weakly mixing. §90 of Knill's *Some Fundamental Theorems in Mathematics*.

Source: P.R. Halmos, 'In general a measure-preserving transformation is mixing', Ann. of Math. (2) 45 (1944) 786–792, and *Lectures on Ergodic Theory*, Chelsea, 1956. Related Baire-category genericity results in ergodic theory: A. Katok and A. Stepin (1967); J.R. Choksi (1965). Listed as §90 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Halmos's proof has two ingredients: (i) **the weak topology is Polish** — by the standard-Borel hypothesis, Aut(X, m) embeds via the Koopman representation into the unitary group of L²(X, m) (with the weak operator topology), and the image carries a separable complete metric; (ii) **weak mixing is a Gδ condition** — `T` is weakly mixing iff for every pair `A, B` of measurable sets, `1/n · ∑_{k<n} |m((T^k)⁻¹ A ∩ B) − m A · m B| → 0`, which is a countable intersection of open conditions (using a countable dense family of measurable sets). For density of the weakly-mixing set, Halmos uses a category argument: dyadic-permutation automorphisms are dense in Aut(X, m) (Rokhlin's lemma), and within each open weak-topology neighbourhood one can produce a weakly mixing automorphism by an explicit small perturbation of a dyadic permutation, so the set of weakly mixing automorphisms is dense. The global ergodicity claim — weakly mixing ⇒ ergodic — is the standard observation that an invariant set `A` with `0 < m A < 1` would force the Cesàro decay to land at `m A · (1 − m A) > 0` instead of 0. Mathlib has `MeasurePreserving`, `Ergodic`, `IsGδ`, `Dense`, and `symmDiff`, but no `Automorphism` bundled type, no weak topology, no `IsWeaklyMixing` predicate, no Rokhlin-style density argument, and no Baire-category framework for the automorphism group.

theorem declaration uses `sorry`generic_weakly_mixing [StandardBorelSpace X]
    (m : Measure X) [IsProbabilityMeasure m] [NoAtoms m] :
    (∃ G : Set (LeanEval.Dynamics.HalmosGenericWeakMixingProblem.Automorphism m), IsGδ G ∧ Dense G ∧
      ∀ T ∈ G, LeanEval.Dynamics.HalmosGenericWeakMixingProblem.IsWeaklyMixing m T) ∧
    (∀ T : LeanEval.Dynamics.HalmosGenericWeakMixingProblem.Automorphism m, LeanEval.Dynamics.HalmosGenericWeakMixingProblem.IsWeaklyMixing m T →
      Ergodic (T.toEquiv : X → X) m) := byX:Type u_1inst✝³:MeasurableSpace Xinst✝²:StandardBorelSpace Xm:Measure Xinst✝¹:IsProbabilityMeasure minst✝:NoAtoms m⊢ (∃ G, IsGδ G ∧ Dense G ∧ ∀ T ∈ G, IsWeaklyMixing m T) ∧
  ∀ (T : Automorphism m), IsWeaklyMixing m T → Ergodic (⇑T.toEquiv) m
  sorryAll goals completed! 🐙

Solved by

Not yet solved.