Genericity of weak mixing

StructureMeasure-preserving automorphism#✓fully proved

An automorphism of a measure space \((X, m)\) is a bijection \(e \colon X \to X\) such that \(e\) and its inverse are measurable and \(e\) preserves \(m\), that is, \(m(e^{-1}(A)) = m(A)\) for every measurable set \(A \subseteq X\).

structure Automorphism (m : Measure X) where
  toEquiv : X ≃ᵐ X
  measurePreserving : MeasurePreserving (toEquiv : X → X) m m

Used by 2

Used byHalmos's theorem: weak mixing is generic · Weakly mixing automorphism

DefinitionWeakly mixing automorphism#✓fully proved

Let \((X, m)\) be a measure space. An automorphism \(T\) of \((X, m)\) is weakly mixing if for all measurable sets \(A, B \subseteq X\),

\[\frac{1}{n} \sum_{k=0}^{n-1} \left| m(T^{-k}(A) \cap B) - m(A) m(B) \right| \to 0\]

as \(n \to \infty\), where \(T^{-k}(A)\) is the preimage of \(A\) under the \(k\)-th iterate of \(T\).

Measures are converted to real numbers here, with an infinite measure counted as \(0\).

def IsWeaklyMixing (m : Measure X) (T : Automorphism m) : Prop :=
  ∀ A B : Set X, MeasurableSet A → MeasurableSet B →
    Tendsto (fun n : ℕ =>
      (∑ k ∈ Finset.range n,
        |(m ((T.toEquiv : X → X)^[k] ⁻¹' A ∩ B)).toReal -
          (m A).toReal * (m B).toReal|) / (n : ℝ))
      atTop (𝓝 0)

Uses 1 · Used by 1

Statement usesMeasure-preserving automorphism

Used byHalmos's theorem: weak mixing is generic

TheoremHalmos's theorem: weak mixing is generic#●ready to prove

Let \(X\) be a standard Borel space and \(m\) a probability measure on \(X\) for which every singleton has measure \(0\). Give the set of automorphisms of \((X, m)\) the weak topology, the topology generated by the sets of automorphisms \(T\) with \(m(T(A) \mathbin{\triangle} T_0(A)) < \varepsilon\), for each automorphism \(T_0\), measurable set \(A \subseteq X\) and real number \(\varepsilon > 0\). Then there is a dense \(G_\delta\) set of automorphisms all of which are weakly mixing, and every weakly mixing automorphism of \((X, m)\) is ergodic for \(m\).

public theorem_wanted generic_weakly_mixing [StandardBorelSpace X]
    (m : Measure X) [IsProbabilityMeasure m] [NullSingletonClass m] :
    (∃ G : Set (Automorphism m), IsGδ G ∧ Dense G ∧
      ∀ T ∈ G, IsWeaklyMixing m T) ∧
    (∀ T : Automorphism m, IsWeaklyMixing m T →
      Ergodic (T.toEquiv : X → X) m)

Sources

• 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). Problem halmos_generic_weak_mixing of the lean-eval benchmark.

Uses 2

Statement usesMeasure-preserving automorphism · Weakly mixing automorphism

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.