Weak-Mixing (Ergodic Theory)

Stream: maths

[Samuel Oettl]

Hi, I'm trying to formalize some (equivalent) definitions of Weak-Mixing. This has lead me to defining measure preserving systems and factors of measure preserving systems.

As a quick note/reminder, a measure preserving system is a quadruple $(X, \mathcal{B}, \mu, T)$ where $X$ is our space, $\mathcal{B}$ is a sigma-algebra on $X$, $\mu$ is a corresponding measure (sometimes automatically assumed to be a probability measure) and $T$ is a (measurable and) measure preserving self map from $X$ to itself. If you want to read more about Ergodic Theory, you can for example look at the book "Ergodic Theory with a view towards Number Theory".

Mathlib already has the structure MeasureTheory.MeasurePreserving.

I now face the following design choice: Should I just use the existing MeasurePreserving structure (possibly extending it when I need the IsProbabilityMeasure assumption)?
Why this could be good:

• Thats how it exists in the library and I'm somewhat new to lean.
• Sometimes in Ergodic Theory we want to look at the same space and map with different Measures or Maps.

Why this could be bad:

• This makes definitions like the product system (which is very much important for weak-mixing) convoluted. Defining factors of systems becomes very convoluted.

What alternative options are there?

I have thought about two (MPS stands for Measure Preserving System):

import Mathlib
namespace MeasureTheory

structure MPS where
  X : Type*
  [mX: MeasurableSpace X]
  μ : Measure X
  [prob: IsProbabilityMeasure μ]
  T : X → X
  measure_preserving : MeasurePreserving T μ μ

end MeasureTheory

and

import Mathlib
namespace MeasureTheory

class MPS (X : Type*) extends MeasureSpace X where
  [prob : IsProbabilityMeasure volume]
  T : X → X
  measure_preserving : MeasurePreserving T volume volume

end MeasureTheory

They both seem reasonable to me and often feel better to work with.

A quite different question is also if I should incorporate the IsProbabilityMeasure assumption into the structure, create a new structure with probability measure instead of measure in the name extending the other structure or just add the IsProbabilityMeasure assumption separately into the theorems and definitions that need it.

Some feedback/thoughts about this would be very much appreciated.
Thank you.

[Sébastien Gouëzel]

The standard design in mathlib is called unbundled: we have spaces, with some properties, and then objects on these spaces. For instance, to define rotations on the circle, we would take advantage of the already existing circle, of its measure, and so on, and then state things about rotations (for instance that they're not weak-mixing).

Your proposed classes MPS go in the opposite direction of bundling many things together. It's a standard practice in other proof assistants (for instance Rocq) but it's not the way we usually do things in mathlib. So my advice would be, instead of your MPS, to define a property IsWeakMixing of a measure-preserving map. And we should also have IsMixing, and so on.

An advantage of this design is that it's very easy to state the theorem that a mixing map is weakly mixing, say. While with the bundled design it would be much more messy: you would need to construct from a bundled mixing system the bundled weakly mixing system.

[Samuel Oettl]

Thank you for your answer. I have rewritten some of my code to (hopefully) correctly reflect this unbundling. Am I roughly on the right track with this?

import Mathlib
namespace MeasureTheory
open Filter Topology
universe u

def weak_mixing1 {X : Type*} [MeasurableSpace X] (μ : Measure X)
(T : X → X) : Prop :=
  ∀ (A B:Set X), (MeasurableSet A ∧ MeasurableSet B) →
  Tendsto (fun n:ℕ ↦
    1/n * (∑ k ∈ Finset.range n, |(μ (A ∩ Set.preimage (T^[k]) B)).toReal
    - (μ A * μ B).toReal|))
  atTop (𝓝 0)

def weak_mixing2 {X : Type*} [MeasurableSpace X] (μ : Measure X) (T : X → X) : Prop :=
  Ergodic (Prod.map T T) (Measure.prod μ μ)

def weak_mixing4 {X : Type u} [MeasurableSpace X] (μ : Measure X) (T : X → X) : Prop :=
  ∀ (Y : Type u) [MeasurableSpace Y], ∀ (ν : Measure Y),
  ∀ (S : Y → Y), Ergodic S ν → Ergodic (Prod.map T S) (Measure.prod μ ν)

lemma one_point_prod_ergodic_imp_ergodic {X : Type*} [MeasurableSpace X] (μ : Measure X) (T : X → X) :
Ergodic (Prod.map T fun y ↦ y) (μ.prod (Measure.dirac PUnit.unit)) → Ergodic T μ := sorry

lemma one_point_ergodic : Ergodic (fun y ↦ y) (Measure.dirac PUnit.unit) := sorry

theorem four_imp_two {X : Type*} [MeasurableSpace X] (μ : Measure X) (T : X → X)
  (h : weak_mixing4 μ T) :
  weak_mixing2 μ T := by
  unfold weak_mixing2
  unfold weak_mixing4 at h
  have h' := h
  specialize h PUnit (Measure.dirac PUnit.unit) (fun (y:PUnit) ↦ y) one_point_ergodic
  apply one_point_prod_ergodic_imp_ergodic at h
  exact h' X μ T h

end MeasureTheory

Note that weak_mixing1 only is a "sensible" definition, if $\mu$ is a probability measure and T is measurable. To have any hope of being equivalent to the other definitions also the assumption that T is measure preserving is needed. Am I correct in only stating this in the theorem (which I haven't proved yet) and not in the definition?

theorem one_imp_four {X : Type*} [MeasurableSpace X] (μ : Measure X)
[IsProbabilityMeasure μ] (T : X → X) (h : MeasurePreserving T μ μ)
  (h : weak_mixing4 μ T) :
  weak_mixing2 μ T := sorry

[Samuel Oettl]

As to be seen in the previous message, in the proof of four implies two we need the fact that if the product of a system with the one point system is ergodic, then the system itself is ergodic. Maybe there is a straightforward brute force proof of this but maybe a more useful, more general proof is proving the fact that every factor of an ergodic system is again ergodic. (I have not thought much about if this is still true for general measure spaces since I have never done ergodic theory on non probability spaces but there is a good chance it is.) To this end I defined factors of systems in the following way:

import Mathlib
namespace MeasureTheory
open Filter Topology

structure subsystem_of {X : Type*} [mX : MeasurableSpace X] (μ : Measure X)
(T : X → X) {Y : Type*} [mY : MeasurableSpace Y]
(ν : Measure Y) (S : Y → Y) where
  toFun : X → Y
  injectivity : Function.Injective toFun
  measurable : MeasurableSet (toFun '' Set.univ)
  restriction_of_sigma_algebra : mY.comap toFun = mX
  restriction_of_measure : Measure.comap toFun ν = μ
  map_compatible : toFun ∘ T = S ∘ toFun
  full_measure : toFun '' Set.univ =ᵐ[ν] Set.univ

structure factor_of {X : Type*} [mX : MeasurableSpace X] (μ : Measure X)
(T : X → X) {Y : Type*} [mY : MeasurableSpace Y] (ν : Measure Y) (S : Y → Y) where
  X' : Type*
  [mX' : MeasurableSpace X']
  μ' : Measure X'
  T' : X' → X'
  is_subsystem1 : subsystem_of μ' T' μ T
  Y' : Type*
  [mY' : MeasurableSpace Y']
  ν' : Measure Y'
  S' : Y' → Y'
  is_subsystem2 : subsystem_of ν' S' ν S
  toFun : Y' → X'
  meas_preserving : MeasurePreserving toFun ν' μ'
  map_compatible : toFun ∘ S' = T' ∘ toFun

end MeasureTheory

This is what seemed convoluted to me. Here if the space, measure and map would be bundled together we could get rid of a lot of lines.
Is this the right approach?

Please let me also know if you need the mathematical definitions of factors of measure preserving systems.

[Lua Viana Reis]

I think that what @Sébastien Gouëzel wrote applies again: instead of having subsystem_of/factor_of, try to work with separate unbundled type classes and structures. Your statement would look something like this:

import Mathlib

open Set Function Filter MeasureTheory MeasureTheory.Measure

variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  (μα : Measure α := by volume_tac) (μβ : Measure β := by volume_tac)
  {f : α → α} {g : β → β} {φ : α → β}

theorem ergodic_of_semiconj (hf : Ergodic f μα)
    (hφ : Semiconj φ f g) (hm : MeasurePreserving φ μα μβ) :
    Ergodic g μβ := by
  sorry

[Lua Viana Reis]

by the way, there is docs#MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_conjugate

[Lua Viana Reis]

Hmm, I guess we may need to assume Measurable g

[Lua Viana Reis]

import Mathlib

open Set Function Filter MeasureTheory Measure

variable {α β γ : Type*} {_ : MeasurableSpace α} {_ : MeasurableSpace β} {_ : MeasurableSpace γ}
  {μα : Measure α} {μβ : Measure β} {f : α → α} {g : β → β} {φ : α → β}

namespace MeasureTheory.MeasurePreserving

theorem map_of_comp {f : α → β} {g : β → γ} {μγ : Measure γ}
    (hgf : MeasurePreserving (g ∘ f) μα μγ) (hg : Measurable g) (hf : Measurable f) :
    MeasurePreserving g (μα.map f) μγ :=
  ⟨hg, (map_map hg hf).trans hgf.map_eq⟩

theorem of_semiconj (hφm : MeasurePreserving φ μα μβ)
    (hf : MeasurePreserving f μα μα) (hφ : Semiconj φ f g) (hg : Measurable g) :
    MeasurePreserving g μβ μβ := by
  have := hφ.comp_eq ▸ hφm.comp hf |>.map_of_comp hg hφm.measurable
  rwa [hφm.map_eq] at this

theorem ergodic_of_semiconj_ergodic (hφm : MeasurePreserving φ μα μβ)
    (hφ : Semiconj φ f g) (hf : Ergodic f μα) (hg : Measurable g) : Ergodic g μβ :=
  ⟨hφm.of_semiconj hf.toMeasurePreserving hφ hg,
   hφm.preErgodic_of_preErgodic_conjugate hf.toPreErgodic hφ⟩

end MeasureTheory.MeasurePreserving

[Lua Viana Reis]

Lua Viana Reis said:

Hmm, I guess we may need to assume Measurable g

I wonder if the semiconjugacy condition imply it is AEMeasurable?

[Lua Viana Reis]

#31793

[Samuel Oettl]

I wonder if the semiconjugacy condition imply it is AEMeasurable?

No, it doesn't even imply NullMeasurable if the following example is correct:
$\alpha$ contains 3 points, the $\sigma$-algebra is the entire powerset, the measure is the sum of the dirac measures at every point and $f$ is a cycle.
$\beta$ also contains 3 points, but the sigma algebra is the one generated by the set only containing the first point. ($g$ and measure on this set are defined in the same way as on the first space)
Now if you take $\phi$ the "identity" it is measure preserving and fulfils the semiconjugacy and $f$ is ergodic.

I'm not 100% certain that $g$ is not NullMeasurable since I haven't thought too much about the way lean constructs a measure from an outer measure, but it seems true.

[Samuel Oettl]

Well, anyway thank you very much for these remarks. This is more than powerful enough to prove what I needed it for. I was not aware that docs#MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_conjugate existed and I was also unaware about Function.Semiconj, thats why I didn't find it.

It is not exactely what I wanted to show. I wanted to show the following:
If $\alpha$ and $\beta$ have measurable subsets of full measure that map that set to itself, and there exists a measure preserving map that maps the first of these subsets to the second, then if the first system is ergodic, so is the second.

[Lua Viana Reis]

Samuel Oettl said:

It is not exactely what I wanted to show. I wanted to show the following:
If $\alpha$ and $\beta$ have measurable subsets of full measure that map that set to itself, and there exists a measure preserving map that maps the first of these subsets to the second, then if the first system is ergodic, so is the second.

Then, what is missing is the lemma stating that if $A \subset \alpha$ is an invariant set of full measure, then $f|_A$ is ergodic if $f$ is. You would get your result by applying it once to show ergodicity of $f|_A$ and using ergodic_of_semiconj_ergodic after that (which doesn't require the factor map to be surjective).

[Lua Viana Reis]

Samuel Oettl said:

I wonder if the semiconjugacy condition imply it is AEMeasurable?

No, it doesn't even imply NullMeasurable if the following example is correct:
$\alpha$ contains 3 points, the $\sigma$-algebra is the entire powerset, the measure is the sum of the dirac measures at every point and $f$ is a cycle.
$\beta$ also contains 3 points, but the sigma algebra is the one generated by the set only containing the first point. ($g$ and measure on this set are defined in the same way as on the first space)
Now if you take $\phi$ the "identity" it is measure preserving and fulfils the semiconjugacy and $f$ is ergodic.

I'm not 100% certain that $g$ is not NullMeasurable since I haven't thought too much about the way lean constructs a measure from an outer measure, but it seems true.

Thanks for the example! I was indeed thinking of NullMeasurable when I wrote it :thinking:

[Lua Viana Reis]

But yes, it is not even NullMeasurable, docs#MeasureTheory.NullMeasurable.aemeasurable show both notions coincide when the sigma-algebra of the codomain is countably generated

[Samuel Oettl]

Lua Viana Reis said:

Samuel Oettl said:

It is not exactely what I wanted to show. I wanted to show the following:
If $\alpha$ and $\beta$ have measurable subsets of full measure that map that set to itself, and there exists a measure preserving map that maps the first of these subsets to the second, then if the first system is ergodic, so is the second.

Then, what is missing is the lemma stating that if $A \subset \alpha$ is an invariant set of full measure, then $f|_A$ is ergodic if $f$ is. You would get your result by applying it once to show ergodicity of $f|_A$ and using ergodic_of_semiconj_ergodic after that (which doesn't require the factor map to be surjective).

Ahh yes, I was suffering from good old tunnel vision, the book I'm working with only defined it like this so it looks more similar to a an isomorphism of measure preserving systems, not because it's actually needed.

[Lua Viana Reis]

Actually, you don't even need to assume $A$ has full measure! Just that it is invariant, so that $f|_A$ makes sense.

[Samuel Oettl]

Lua Viana Reis said:

But yes, it is not even NullMeasurable, docs#MeasureTheory.NullMeasurable.aemeasurable show both notions coincide when the sigma-algebra of the codomain is countably generated

For completeness: AEMeasurable implies NullMeasurable (in case anyone doesn‘t already know when reading this discussion)
docs#AEMeasurable.nullMeasurable

[Notification Bot]

22 messages were moved from this topic to #maths > Stating that a set is backwards invariant by Lua Viana Reis.

[Samuel Oettl]

I don't know if I should create a new topic for this but I encountered two more obstacles:

Firstly I need the result that for f and g in Lp (I only need it for p=2) the function fun z ↦ f z.1 * g z.2 is also in Lp wrt. the product measure (under the assumption that one of the measures is SFinite). I was only able to locate docs#MeasureTheory.lintegral_prod_mul which of course can be used to show the result I want, but it's only 80% there.
I also need the result that the complex conjugation of an Lp function is in Lp. Does that already exist somewhere?

Secondly I want the Filter on the natural numbers consisting of the sets of density one. (So sets of the from $A \subseteq \mathbb{N}$ s.t. $\lim_{n \to \infty} \frac{|A \cap \{1,2,\dots,n\}|}{n} = 1$) Does this already exist in mathlib?

[Sébastien Gouëzel]

For your first question, I don't think it's there in the form you need, so you will need to prove it using the lemma you mention. The fact that the complex conjugate is in L^p should follow from docs#MeasureTheory.MemLp.continuousLinearMap_comp using docs#Complex.conjCLE.

[Sébastien Gouëzel]

For sets of density one, we don't have it either; see a recent discussion at #Is there code for X? > natural density @ 💬

[Samuel Oettl]

Great, thank you very much.