feat(dynamics/ergodic): define measure preserving maps (#6764)

Also prove some missing lemmas about measures.

Author: urkud

src/data/set/basic.lean

@@ -1971,6 +1971,10 @@ lemma prod_preimage_left {f : γ → α} : (f ⁻¹' s).prod t = (λp, (f p.1, p
 
 lemma prod_preimage_right {g : δ → β} : s.prod (g ⁻¹' t) = (λp, (p.1, g p.2)) ⁻¹' (s.prod t) := rfl
 
+lemma preimage_prod_map_prod (f : α → β) (g : γ → δ) (s : set β) (t : set δ) :
+  prod.map f g ⁻¹' (s.prod t) = (f ⁻¹' s).prod (g ⁻¹' t) :=
+rfl
+
 lemma mk_preimage_prod (f : γ → α) (g : γ → β) :
   (λ x, (f x, g x)) ⁻¹' s.prod t = f ⁻¹' s ∩ g ⁻¹' t := rfl
 
@@ -2014,7 +2018,7 @@ theorem image_swap_prod : prod.swap '' t.prod s = s.prod t :=
 by rw [image_swap_eq_preimage_swap, preimage_swap_prod]
 
 theorem prod_image_image_eq {m₁ : α → γ} {m₂ : β → δ} :
-  (image m₁ s).prod (image m₂ t) = image (λp:α×β, (m₁ p.1, m₂ p.2)) (s.prod t) :=
+  (m₁ '' s).prod (m₂ '' t) = image (λp:α×β, (m₁ p.1, m₂ p.2)) (s.prod t) :=
 ext $ by simp [-exists_and_distrib_right, exists_and_distrib_right.symm, and.left_comm,
   and.assoc, and.comm]
 

src/dynamics/ergodic/measure_preserving.lean

@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import measure_theory.prod
+
+/-!
+# Measure preserving maps
+
+We say that `f : α → β` is a measure preserving map w.r.t. measures `μ : measure α` and
+`ν : measure β` if `f` is measurable and `map f μ = ν`. In this file we define the predicate
+`measure_theory.measure_preserving` and prove its basic properties.
+
+We use the term "measure preserving" because in many applications `α = β` and `μ = ν`.
+
+## References
+
+Partially based on
+[this](https://www.isa-afp.org/browser_info/current/AFP/Ergodic_Theory/Measure_Preserving_Transformations.html)
+Isabelle formalization.
+
+## Tags
+
+measure preserving map, measure
+-/
+
+variables {α β γ δ : Type*} [measurable_space α] [measurable_space β] [measurable_space γ]
+  [measurable_space δ]
+
+namespace measure_theory
+
+open measure function set
+
+variables {μa : measure α} {μb : measure β} {μc : measure γ} {μd : measure δ}
+
+/-- `f` is a measure preserving map w.r.t. measures `μa` and `μb` if `f` is measurable
+and `map f μa = μb`. -/
+@[protect_proj]
+structure measure_preserving (f : α → β) (μa : measure α . volume_tac)
+  (μb : measure β . volume_tac) : Prop :=
+(measurable : measurable f)
+(map_eq : map f μa = μb)
+
+namespace measure_preserving
+
+protected lemma id (μ : measure α) : measure_preserving id μ μ :=
+⟨measurable_id, map_id⟩
+
+protected lemma quasi_measure_preserving {f : α → β} (hf : measure_preserving f μa μb) :
+  quasi_measure_preserving f μa μb :=
+⟨hf.1, hf.2.absolutely_continuous⟩
+
+lemma comp {g : β → γ} {f : α → β} (hg : measure_preserving g μb μc)
+  (hf : measure_preserving f μa μb) :
+  measure_preserving (g ∘ f) μa μc :=
+⟨hg.1.comp hf.1, by rw [← map_map hg.1 hf.1, hf.2, hg.2]⟩
+
+protected lemma sigma_finite {f : α → β} (hf : measure_preserving f μa μb) [sigma_finite μb] :
+  sigma_finite μa :=
+sigma_finite.of_map μa hf.1 (by rwa hf.map_eq)
+
+lemma measure_preimage {f : α → β} (hf : measure_preserving f μa μb)
+  {s : set β} (hs : measurable_set s) :
+  μa (f ⁻¹' s) = μb s :=
+by rw [← hf.map_eq, map_apply hf.1 hs]
+
+protected lemma iterate {f : α → α} (hf : measure_preserving f μa μa) :
+  ∀ n, measure_preserving (f^[n]) μa μa
+| 0 := measure_preserving.id μa
+| (n + 1) := (iterate n).comp hf
+
+lemma skew_product [sigma_finite μb] [sigma_finite μd]
+  {f : α → β} (hf : measure_preserving f μa μb) {g : α → γ → δ}
+  (hgm : measurable (uncurry g)) (hg : ∀ᵐ x ∂μa, map (g x) μc = μd) :
+  measure_preserving (λ p : α × γ, (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd) :=
+begin
+  classical,
+  have : measurable (λ p : α × γ, (f p.1, g p.1 p.2)) := (hf.1.comp measurable_fst).prod_mk hgm,
+  /- if `μa = 0`, then the lemma is trivial, otherwise we can use `hg`
+  to deduce `sigma_finite μc`. -/
+  by_cases ha : μa = 0,
+  { rw [← hf.map_eq, ha, zero_prod, (map f).map_zero, zero_prod],
+    exact ⟨this, (map _).map_zero⟩ },
+  haveI : μa.ae.ne_bot := ae_ne_bot.2 ha,
+  rcases hg.exists with ⟨x, hx⟩,
+  haveI : sigma_finite μc := sigma_finite.of_map _ hgm.of_uncurry_left (by rwa hx),
+  clear hx x,
+  refine ⟨this, (prod_eq $ λ s t hs ht, _).symm⟩,
+  rw [map_apply this (hs.prod ht)],
+  refine (prod_apply (this $ hs.prod ht)).trans _,
+  have : ∀ᵐ x ∂μa, μc ((λ y, (f x, g x y)) ⁻¹' s.prod t) = indicator (f ⁻¹' s) (λ y, μd t) x,
+  { refine hg.mono (λ x hx, _),
+    simp only [mk_preimage_prod_right_fn_eq_if, indicator_apply, mem_preimage],
+    split_ifs,
+    { rw [← map_apply hgm.of_uncurry_left ht, hx] },
+    { exact measure_empty } },
+  simp only [preimage_preimage],
+  rw [lintegral_congr_ae this, lintegral_indicator _ (hf.1 hs),
+    set_lintegral_const, hf.measure_preimage hs, mul_comm]
+end
+
+/-- If `f : α → β` sends the measure `μa` to `μb` and `g : γ → δ` sends the measure `μc` to `μd`,
+then `prod.map f g` sends `μa.prod μc` to `μb.prod μd`. -/
+lemma prod [sigma_finite μb] [sigma_finite μd] {f : α → β} {g : γ → δ}
+  (hf : measure_preserving f μa μb) (hg : measure_preserving g μc μd) :
+  measure_preserving (prod.map f g) (μa.prod μc) (μb.prod μd) :=
+have measurable (uncurry $ λ _ : α, g), from (hg.1.comp measurable_snd),
+hf.skew_product this $ filter.eventually_of_forall $ λ _, hg.map_eq
+
+end measure_preserving
+
+end measure_theory

src/measure_theory/giry_monad.lean

@@ -98,6 +98,9 @@ measure.of_measurable
   ∀{s : set α}, measurable_set s → join m s = ∫⁻ μ, μ s ∂m :=
 measure.of_measurable_apply
 
+@[simp] lemma join_zero : (0 : measure (measure α)).join = 0 :=
+by { ext1 s hs, simp [hs] }
+
 lemma measurable_join : measurable (join : measure (measure α) → measure α) :=
 measurable_of_measurable_coe _ $ assume s hs,
   by simp only [join_apply hs]; exact measurable_lintegral (measurable_coe hs)
@@ -152,6 +155,22 @@ end
 functions. When the function `f` is not measurable the result is not well defined. -/
 def bind (m : measure α) (f : α → measure β) : measure β := join (map f m)
 
+@[simp] lemma bind_zero_left (f : α → measure β) : bind 0 f = 0 :=
+by simp [bind]
+
+@[simp] lemma bind_zero_right (m : measure α) :
+  bind m (0 : α → measure β) = 0 :=
+begin
+  ext1 s hs,
+  simp only [bind, hs, join_apply, coe_zero, pi.zero_apply],
+  rw [lintegral_map (measurable_coe hs) measurable_zero],
+  simp
+end
+
+@[simp] lemma bind_zero_right' (m : measure α) :
+  bind m (λ _, 0 : α → measure β) = 0 :=
+bind_zero_right m
+
 @[simp] lemma bind_apply {m : measure α} {f : α → measure β} {s : set β}
   (hs : measurable_set s) (hf : measurable f) :
   bind m f s = ∫⁻ a, f a s ∂m :=

src/measure_theory/measurable_space.lean

@@ -696,6 +696,10 @@ measurable_const.prod_mk measurable_id
 lemma measurable_prod_mk_right {y : β} : measurable (λ x : α, (x, y)) :=
 measurable_id.prod_mk measurable_const
 
+lemma measurable.prod_map [measurable_space δ] {f : α → β} {g : γ → δ} (hf : measurable f)
+  (hg : measurable g) : measurable (prod.map f g) :=
+(hf.comp measurable_fst).prod_mk (hg.comp measurable_snd)
+
 lemma measurable.of_uncurry_left {f : α → β → γ} (hf : measurable (uncurry f)) {x : α} :
   measurable (f x) :=
 hf.comp measurable_prod_mk_left

src/measure_theory/measure_space.lean

@@ -1473,6 +1473,9 @@ open measure
 @[simp] lemma ae_eq_bot : μ.ae = ⊥ ↔ μ = 0 :=
 by rw [← empty_in_sets_eq_bot, mem_ae_iff, compl_empty, measure_univ_eq_zero]
 
+@[simp] lemma ae_ne_bot : μ.ae.ne_bot ↔ μ ≠ 0 :=
+ne_bot_iff.trans (not_congr ae_eq_bot)
+
 @[simp] lemma ae_zero : (0 : measure α).ae = ⊥ := ae_eq_bot.2 rfl
 
 @[mono] lemma ae_mono {μ ν : measure α} (h : μ ≤ ν) : μ.ae ≤ ν.ae :=
@@ -1823,7 +1826,7 @@ lemma sigma_finite_of_not_nonempty (μ : measure α) (hα : ¬ nonempty α) : si
 ⟨⟨⟨λ _, ∅, λ n, measurable_set.empty, λ n, by simp, by simp [eq_empty_of_not_nonempty hα univ]⟩⟩⟩
 
 lemma sigma_finite_of_countable {S : set (set α)} (hc : countable S)
-  (hμ : ∀ s ∈ S, μ s < ∞)  (hU : ⋃₀ S = univ) :
+  (hμ : ∀ s ∈ S, μ s < ∞) (hU : ⋃₀ S = univ) :
   sigma_finite μ :=
 begin
   obtain ⟨s, hμ, hs⟩ : ∃ s : ℕ → set α, (∀ n, μ (s n) < ∞) ∧ (⋃ n, s n) = univ,
@@ -1852,7 +1855,7 @@ instance sum.sigma_finite {ι} [fintype ι] (μ : ι → measure α) [∀ i, sig
 begin
   haveI : encodable ι := (encodable.trunc_encodable_of_fintype ι).out,
   have : ∀ n, measurable_set (⋂ (i : ι), spanning_sets (μ i) n) :=
-  λ n, measurable_set.Inter (λ i, measurable_spanning_sets (μ i) n),
+    λ n, measurable_set.Inter (λ i, measurable_spanning_sets (μ i) n),
   refine ⟨⟨⟨λ n, ⋂ i, spanning_sets (μ i) n, this, λ n, _, _⟩⟩⟩,
   { rw [sum_apply _ (this n), tsum_fintype, ennreal.sum_lt_top_iff],
     rintro i -,
@@ -1865,6 +1868,14 @@ instance add.sigma_finite (μ ν : measure α) [sigma_finite μ] [sigma_finite 
   sigma_finite (μ + ν) :=
 by { rw [← sum_cond], refine @sum.sigma_finite _ _ _ _ _ (bool.rec _ _); simpa }
 
+lemma sigma_finite.of_map (μ : measure α) {f : α → β} (hf : measurable f)
+  (h : sigma_finite (map f μ)) :
+  sigma_finite μ :=
+⟨⟨⟨λ n, f ⁻¹' (spanning_sets (map f μ) n),
+   λ n, hf $ measurable_spanning_sets _ _,
+   λ n, by simp only [← map_apply hf, measurable_spanning_sets, measure_spanning_sets_lt_top],
+   by rw [← preimage_Union, Union_spanning_sets, preimage_univ]⟩⟩⟩
+
 /-- A measure is called locally finite if it is finite in some neighborhood of each point. -/
 class locally_finite_measure [topological_space α] (μ : measure α) : Prop :=
 (finite_at_nhds : ∀ x, μ.finite_at_filter (𝓝 x))

src/measure_theory/prod.lean

@@ -540,6 +540,23 @@ by { refine prod_eq (λ s t hs ht, _), simp_rw [add_apply, prod_prod hs ht, left
 lemma add_prod (μ' : measure α) [sigma_finite μ'] : (μ + μ').prod ν = μ.prod ν + μ'.prod ν :=
 by { refine prod_eq (λ s t hs ht, _), simp_rw [add_apply, prod_prod hs ht, right_distrib] }
 
+@[simp] lemma zero_prod (ν : measure β) : (0 : measure α).prod ν = 0 :=
+by { rw measure.prod, exact bind_zero_left _ }
+
+@[simp] lemma prod_zero (μ : measure α) : μ.prod (0 : measure β) = 0 :=
+by simp [measure.prod]
+
+lemma map_prod_map {δ} [measurable_space δ] {f : α → β} {g : γ → δ}
+  {μa : measure α} {μc : measure γ} (hfa : sigma_finite (map f μa))
+  (hgc : sigma_finite (map g μc)) (hf : measurable f) (hg : measurable g) :
+  (map f μa).prod (map g μc) = map (prod.map f g) (μa.prod μc) :=
+begin
+  haveI := hgc.of_map μc hg,
+  refine prod_eq (λ s t hs ht, _),
+  rw [map_apply (hf.prod_map hg) (hs.prod ht), map_apply hf hs, map_apply hg ht],
+  exact prod_prod (hf hs) (hg ht)
+end
+
 end measure
 end measure_theory