feat(measure_theory): measure preserving maps and integrals (#10326)

If `f` is a measure preserving map, then `∫ y, g y ∂ν = ∫ x, g (f x) ∂μ`. It was two rewrites with the old API (`hf.map_eq`, then a lemma about integral over map measure); it's one `rw` now.

Also add versions for special cases when `f` is a measurable embedding (in this case we don't need to assume measurability of `g`).

src/data/equiv/fin.lean

@@ -50,6 +50,19 @@ non-dependent version and `prod_equiv_pi_fin_two` for a version with inputs `α
   left_inv := λ f, funext $ fin.forall_fin_two.2 ⟨rfl, rfl⟩,
   right_inv := λ ⟨x, y⟩, rfl }
 
+lemma fin.preimage_apply_01_prod {α : fin 2 → Type u} (s : set (α 0)) (t : set (α 1)) :
+  (λ f : Π i, α i, (f 0, f 1)) ⁻¹' (s.prod t) =
+    set.pi set.univ (fin.cons s $ fin.cons t fin.elim0) :=
+begin
+  ext f,
+  have : (fin.cons s (fin.cons t fin.elim0) : Π i, set (α i)) 1 = t := rfl,
+  simp [fin.forall_fin_two, this]
+end
+
+lemma fin.preimage_apply_01_prod' {α : Type u} (s t : set α) :
+  (λ f : fin 2 → α, (f 0, f 1)) ⁻¹' (s.prod t) = set.pi set.univ ![s, t] :=
+fin.preimage_apply_01_prod s t
+
 /-- A product space `α × β` is equivalent to the space `Π i : fin 2, γ i`, where
 `γ = fin.cons α (fin.cons β fin_zero_elim)`. See also `pi_fin_two_equiv` and
 `fin_two_arrow_equiv`. -/

src/dynamics/ergodic/measure_preserving.lean

@@ -42,6 +42,11 @@ structure measure_preserving (f : α → β) (μa : measure α . volume_tac)
 (measurable : measurable f)
 (map_eq : map f μa = μb)
 
+protected lemma _root_.measurable.measure_preserving {f : α → β}
+  (h : measurable f) (μa : measure α) :
+  measure_preserving f μa (map f μa) :=
+⟨h, rfl⟩
+
 namespace measure_preserving
 
 protected lemma id (μ : measure α) : measure_preserving id μ μ :=
@@ -52,6 +57,19 @@ lemma symm {e : α ≃ᵐ β} {μa : measure α} {μb : measure β} (h : measure
 ⟨e.symm.measurable,
   by rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]⟩
 
+lemma restrict_preimage {f : α → β} (hf : measure_preserving f μa μb) {s : set β}
+  (hs : measurable_set s) : measure_preserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s) :=
+⟨hf.measurable, by rw [← hf.map_eq, restrict_map hf.measurable hs]⟩
+
+lemma restrict_preimage_emb {f : α → β} (hf : measure_preserving f μa μb)
+  (h₂ : measurable_embedding f) (s : set β) :
+  measure_preserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s) :=
+⟨hf.measurable, by rw [← hf.map_eq, h₂.restrict_map]⟩
+
+lemma restrict_image_emb {f : α → β} (hf : measure_preserving f μa μb) (h₂ : measurable_embedding f)
+  (s : set α) : measure_preserving f (μa.restrict s) (μb.restrict (f '' s)) :=
+by simpa only [preimage_image_eq _ h₂.injective] using hf.restrict_preimage_emb h₂ (f '' s)
+
 protected lemma quasi_measure_preserving {f : α → β} (hf : measure_preserving f μa μb) :
   quasi_measure_preserving f μa μb :=
 ⟨hf.1, hf.2.absolutely_continuous⟩

src/measure_theory/constructions/pi.lean

@@ -54,6 +54,8 @@ noncomputable theory
 open function set measure_theory.outer_measure filter measurable_space encodable
 open_locale classical big_operators topological_space ennreal
 
+universes u v
+
 variables {ι ι' : Type*} {α : ι → Type*}
 
 /-! We start with some measurability properties -/
@@ -364,21 +366,6 @@ lemma pi_closed_ball [∀ i, metric_space (α i)] (x : Π i, α i) {r : ℝ}
   measure.pi μ (metric.closed_ball x r) = ∏ i, μ i (metric.closed_ball (x i) r) :=
 by rw [closed_ball_pi _ hr, pi_pi]
 
-lemma pi_unique_eq_map {β : Type*} {m : measurable_space β} (μ : measure β) (α : Type*) [unique α] :
-  measure.pi (λ a : α, μ) = map (measurable_equiv.fun_unique α β).symm μ :=
-begin
-  set e := measurable_equiv.fun_unique α β,
-  have : pi_premeasure (λ _ : α, μ.to_outer_measure) = map e.symm μ,
-  { ext1 s,
-    rw [pi_premeasure, fintype.prod_unique, to_outer_measure_apply, e.symm.map_apply],
-    congr' 1, exact e.to_equiv.image_eq_preimage s },
-  simp only [measure.pi, outer_measure.pi, this, bounded_by_measure, to_outer_measure_to_measure],
-end
-
-lemma map_fun_unique {α β : Type*} [unique α] {m : measurable_space β} (μ : measure β) :
-  map (measurable_equiv.fun_unique α β) (measure.pi $ λ _, μ) = μ :=
-(measurable_equiv.fun_unique α β).map_apply_eq_iff_map_symm_apply_eq.2 (pi_unique_eq_map μ _).symm
-
 instance pi.sigma_finite : sigma_finite (measure.pi μ) :=
 (finite_spanning_sets_in.pi (λ i, (μ i).to_finite_spanning_sets_in)).sigma_finite
 
@@ -392,36 +379,6 @@ begin
   exact is_empty_elim
 end
 
-lemma {u} pi_fin_two_eq_map {α : fin 2 → Type u} {m : Π i, measurable_space (α i)}
-  (μ : Π i, measure (α i)) [∀ i, sigma_finite (μ i)] :
-  measure.pi μ = map (measurable_equiv.pi_fin_two α).symm ((μ 0).prod (μ 1)) :=
-begin
-  refine pi_eq (λ s hs, _),
-  rw [measurable_equiv.map_apply, fin.prod_univ_succ, fin.prod_univ_succ, fin.prod_univ_zero,
-    mul_one, ← measure.prod_prod],
-  congr' 1,
-  ext ⟨a, b⟩,
-  simp [fin.forall_fin_succ, is_empty.forall_iff]
-end
-
-lemma {u} map_pi_fin_two {α : fin 2 → Type u} {m : Π i, measurable_space (α i)}
-  (μ : Π i, measure (α i)) [∀ i, sigma_finite (μ i)] :
-  map (measurable_equiv.pi_fin_two α) (measure.pi μ) = ((μ 0).prod (μ 1)) :=
-(measurable_equiv.pi_fin_two α).map_apply_eq_iff_map_symm_apply_eq.2 (pi_fin_two_eq_map μ).symm
-
-lemma prod_eq_map_fin_two_arrow {α : Type*} {m : measurable_space α} (μ ν : measure α)
-  [sigma_finite μ] [sigma_finite ν] :
-  μ.prod ν = map measurable_equiv.fin_two_arrow (measure.pi ![μ, ν]) :=
-begin
-  haveI : ∀ i, sigma_finite (![μ, ν] i) := fin.forall_fin_two.2 ⟨‹_›, ‹_›⟩,
-  exact (map_pi_fin_two ![μ, ν]).symm
-end
-
-lemma prod_eq_map_fin_two_arrow_same {α : Type*} {m : measurable_space α} (μ : measure α)
-  [sigma_finite μ] :
-  μ.prod μ = map measurable_equiv.fin_two_arrow (measure.pi $ λ _, μ) :=
-by rw [prod_eq_map_fin_two_arrow, matrix.vec_single_eq_const, matrix.vec_cons_const]
-
 lemma pi_eval_preimage_null {i : ι} {s : set (α i)} (hs : μ i s = 0) :
   measure.pi μ (eval i ⁻¹' s) = 0 :=
 begin
@@ -576,7 +533,6 @@ begin
 end
 
 end measure
-
 instance measure_space.pi [Π i, measure_space (α i)] : measure_space (Π i, α i) :=
 ⟨measure.pi (λ i, volume)⟩
 
@@ -599,114 +555,83 @@ lemma volume_pi_closed_ball [Π i, measure_space (α i)] [∀ i, sigma_finite (v
   volume (metric.closed_ball x r) = ∏ i, volume (metric.closed_ball (x i) r) :=
 measure.pi_closed_ball _ _ hr
 
-section fun_unique
 /-!
-### Integral over `ι → α` with `[unique ι]`
+### Measure preserving equivalences
 
-In this section we prove some lemmas that relate integrals over `ι → β`, where `ι` is a type with
-unique element (e.g., `unit` or `fin 1`) and integrals over `β`.
+In this section we prove that some measurable equivalences (e.g., between `fin 1 → α` and `α` or
+between `fin 2 → α` and `α × α`) preserve measure or volume. These lemmas can be used to prove that
+measures of corresponding sets (images or preimages) have equal measures and functions `f ∘ e` and
+`f` have equal integrals, see lemmas in the `measure_theory.measure_preserving` prefix.
 -/
 
-variables {β E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E]
-  [topological_space.second_countable_topology E] [borel_space E] [complete_space E]
-
-lemma integral_fun_unique_pi (ι) [unique ι] {m : measurable_space β} (μ : measure β)
-  (f : (ι → β) → E) :
-  ∫ y, f y ∂(measure.pi (λ _, μ)) = ∫ x, f (λ _, x) ∂μ :=
-by rw [measure.pi_unique_eq_map μ ι, integral_map_equiv]; refl
-
-lemma integral_fun_unique_pi' (ι : Type*) [unique ι] {m : measurable_space β} (μ : measure β)
-  (f : β → E) :
-  ∫ y : ι → β, f (y (default ι)) ∂(measure.pi (λ _, μ)) = ∫ x, f x ∂μ :=
-integral_fun_unique_pi ι μ _
-
-lemma integral_fun_unique (ι : Type*) [unique ι] [measure_space β] (f : (ι → β) → E) :
-  ∫ y, f y = ∫ x, f (λ _, x) :=
-integral_fun_unique_pi ι volume f
-
-lemma integral_fun_unique' (ι : Type*) [unique ι] [measure_space β] (f : β → E) :
-  ∫ y : ι → β, f (y (default ι)) = ∫ x, f x :=
-integral_fun_unique_pi' ι volume f
+section measure_preserving
 
-lemma set_integral_fun_unique_pi (ι : Type*) [unique ι] {m : measurable_space β} (μ : measure β)
-  (f : (ι → β) → E) (s : set (ι → β)) :
-  ∫ y in s, f y ∂(measure.pi (λ _, μ)) = ∫ x in const ι ⁻¹' s, f (λ _, x) ∂μ :=
-by rw [measure.pi_unique_eq_map μ ι, set_integral_map_equiv]; refl
-
-lemma set_integral_fun_unique_pi' (ι : Type*) [unique ι] {m : measurable_space β} (μ : measure β)
-  (f : β → E) (s : set β) :
-  ∫ y : ι → β in function.eval (default ι) ⁻¹' s, f (y (default ι)) ∂(measure.pi (λ _, μ)) =
-    ∫ x in s, f x ∂μ :=
-by erw [set_integral_fun_unique_pi, (equiv.fun_unique ι β).symm_preimage_preimage]
-
-lemma set_integral_fun_unique (ι : Type*) [unique ι] [measure_space β] (f : (ι → β) → E)
-  (s : set (ι → β)) :
-  ∫ y in s, f y = ∫ x in const ι ⁻¹' s, f (λ _, x) :=
-by convert set_integral_fun_unique_pi ι volume f s
-
-lemma set_integral_fun_unique' (ι : Type*) [unique ι] [measure_space β] (f : β → E) (s : set β) :
-  ∫ y : ι → β in @function.eval ι (λ _, β) (default ι) ⁻¹' s, f (y (default ι)) = ∫ x in s, f x :=
-by convert set_integral_fun_unique_pi' ι volume f s
+lemma measure_preserving_fun_unique {β : Type u} {m : measurable_space β} (μ : measure β)
+  (α : Type v) [unique α] :
+  measure_preserving (measurable_equiv.fun_unique α β) (measure.pi (λ a : α, μ)) μ :=
+begin
+  set e := measurable_equiv.fun_unique α β,
+  have : pi_premeasure (λ _ : α, μ.to_outer_measure) = measure.map e.symm μ,
+  { ext1 s,
+    rw [pi_premeasure, fintype.prod_unique, to_outer_measure_apply, e.symm.map_apply],
+    congr' 1, exact e.to_equiv.image_eq_preimage s },
+  simp only [measure.pi, outer_measure.pi, this, bounded_by_measure, to_outer_measure_to_measure],
+  exact ((measurable_equiv.fun_unique α β).symm.measurable.measure_preserving _).symm
+end
 
-end fun_unique
+lemma volume_preserving_fun_unique (α : Type u) (β : Type v) [unique α] [measure_space β] :
+  measure_preserving (measurable_equiv.fun_unique α β) volume volume :=
+measure_preserving_fun_unique volume α
 
-section fin_two_arrow
+lemma measure_preserving_pi_fin_two {α : fin 2 → Type u} {m : Π i, measurable_space (α i)}
+  (μ : Π i, measure (α i)) [∀ i, sigma_finite (μ i)] :
+  measure_preserving (measurable_equiv.pi_fin_two α) (measure.pi μ) ((μ 0).prod (μ 1)) :=
+begin
+  refine ⟨measurable_equiv.measurable _, (measure.prod_eq $ λ s t hs ht, _).symm⟩,
+  rw [measurable_equiv.map_apply, measurable_equiv.pi_fin_two_apply, fin.preimage_apply_01_prod,
+    measure.pi_pi, fin.prod_univ_two],
+  refl
+end
 
-variables {β E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E]
-  [topological_space.second_countable_topology E] [borel_space E] [complete_space E]
+lemma volume_preserving_pi_fin_two (α : fin 2 → Type u) [Π i, measure_space (α i)]
+  [∀ i, sigma_finite (volume : measure (α i))] :
+  measure_preserving (measurable_equiv.pi_fin_two α) volume volume :=
+measure_preserving_pi_fin_two _
 
-lemma integral_fin_two_arrow_pi {m : measurable_space β} (μ ν : measure β)
-  [sigma_finite μ] [sigma_finite ν] (f : (fin 2 → β) → E) :
-  ∫ y, f y ∂(measure.pi ![μ, ν]) = ∫ x, f ![x.1, x.2] ∂(μ.prod ν) :=
+lemma measure_preserving_fin_two_arrow_vec {α : Type u} {m : measurable_space α}
+  (μ ν : measure α) [sigma_finite μ] [sigma_finite ν] :
+  measure_preserving measurable_equiv.fin_two_arrow (measure.pi ![μ, ν]) (μ.prod ν) :=
 begin
   haveI : ∀ i, sigma_finite (![μ, ν] i) := fin.forall_fin_two.2 ⟨‹_›, ‹_›⟩,
-  rw [measure.pi_fin_two_eq_map, integral_map_equiv], refl
+  exact measure_preserving_pi_fin_two _
 end
 
-lemma integral_fin_two_arrow_pi' {m : measurable_space β} (μ ν : measure β) [sigma_finite μ]
-  [sigma_finite ν] (f : β × β → E) :
-  ∫ y : fin 2 → β, f (y 0, y 1) ∂(measure.pi ![μ, ν]) = ∫ x, f x ∂(μ.prod ν) :=
-by { rw [measure.prod_eq_map_fin_two_arrow, integral_map_equiv], refl }
-
-lemma integral_fin_two_arrow [measure_space β] [sigma_finite (volume : measure β)]
-  (f : (fin 2 → β) → E) :
-  ∫ y, f y = ∫ x : β × β, f ![x.1, x.2] :=
-by rw [volume_pi, measure.volume_eq_prod, ← integral_fin_two_arrow_pi, matrix.vec_single_eq_const,
-  matrix.vec_cons_const]
-
-lemma integral_fin_two_arrow' [measure_space β] [sigma_finite (volume : measure β)]
-  (f : β × β → E) :
-  ∫ y : fin 2 → β, f (y 0, y 1) = ∫ x, f x :=
-by rw [volume_pi, measure.volume_eq_prod, ← integral_fin_two_arrow_pi', matrix.vec_single_eq_const,
-  matrix.vec_cons_const]
-
-lemma set_integral_fin_two_arrow_pi {m : measurable_space β} (μ ν : measure β)
-  [sigma_finite μ] [sigma_finite ν] (f : (fin 2 → β) → E) (s : set (fin 2 → β)) :
-  ∫ y in s, f y ∂(measure.pi ![μ, ν]) =
-    ∫ x : β × β in (fin_two_arrow_equiv β).symm ⁻¹' s, f ![x.1, x.2] ∂(μ.prod ν) :=
+lemma measure_preserving_fin_two_arrow {α : Type u} {m : measurable_space α}
+  (μ : measure α) [sigma_finite μ] :
+  measure_preserving measurable_equiv.fin_two_arrow (measure.pi (λ _, μ)) (μ.prod μ) :=
+by simpa only [matrix.vec_single_eq_const, matrix.vec_cons_const]
+  using measure_preserving_fin_two_arrow_vec μ μ
+
+lemma volume_preserving_fin_two_arrow (α : Type u) [measure_space α]
+  [sigma_finite (volume : measure α)] :
+  measure_preserving (@measurable_equiv.fin_two_arrow α _) volume volume :=
+measure_preserving_fin_two_arrow volume
+
+lemma measure_preserving_pi_empty {ι : Type u} {α : ι → Type v} [is_empty ι]
+  {m : Π i, measurable_space (α i)} (μ : Π i, measure (α i)) :
+  measure_preserving (measurable_equiv.of_unique_of_unique (Π i, α i) unit)
+    (measure.pi μ) (measure.dirac ()) :=
 begin
-  haveI : ∀ i, sigma_finite (![μ, ν] i) := fin.forall_fin_two.2 ⟨‹_›, ‹_›⟩,
-  rw [measure.pi_fin_two_eq_map, set_integral_map_equiv], refl
+  set e := (measurable_equiv.of_unique_of_unique (Π i, α i) unit),
+  refine ⟨e.measurable, _⟩,
+  rw [measure.pi_of_empty, measure.map_dirac e.measurable], refl
 end
 
-lemma set_integral_fin_two_arrow_pi' {m : measurable_space β} (μ ν : measure β)
-  [sigma_finite μ] [sigma_finite ν] (f : β × β → E) (s : set (β × β)) :
-  ∫ y : fin 2 → β in fin_two_arrow_equiv β ⁻¹' s, f (y 0, y 1) ∂(measure.pi ![μ, ν]) =
-    ∫ x in s, f x ∂(μ.prod ν) :=
-by { rw [set_integral_fin_two_arrow_pi, equiv.symm_preimage_preimage], simp }
-
-lemma set_integral_fin_two_arrow [measure_space β] [sigma_finite (volume : measure β)]
-  (f : (fin 2 → β) → E) (s : set (fin 2 → β)) :
-  ∫ y in s, f y = ∫ x in (fin_two_arrow_equiv β).symm ⁻¹' s, f ![x.1, x.2] :=
-by rw [measure.volume_eq_prod, ← set_integral_fin_two_arrow_pi, volume_pi,
-  matrix.vec_single_eq_const, matrix.vec_cons_const]
-
-lemma set_integral_fin_two_arrow' [measure_space β] [sigma_finite (volume : measure β)]
-  (f : β × β → E) (s : set (β × β)) :
-  ∫ y : fin 2 → β in fin_two_arrow_equiv β ⁻¹' s, f (y 0, y 1) = ∫ x in s, f x :=
-by rw [measure.volume_eq_prod, ← set_integral_fin_two_arrow_pi', volume_pi,
-  matrix.vec_single_eq_const, matrix.vec_cons_const]
-
-end fin_two_arrow
+lemma volume_preserving_pi_empty {ι : Type u} (α : ι → Type v) [is_empty ι]
+  [Π i, measure_space (α i)] :
+  measure_preserving (measurable_equiv.of_unique_of_unique (Π i, α i) unit) volume volume :=
+measure_preserving_pi_empty (λ _, volume)
+
+end measure_preserving
 
 end measure_theory

src/measure_theory/function/l1_space.lean

@@ -466,6 +466,16 @@ lemma integrable_map_equiv (f : α ≃ᵐ δ) (g : δ → β) :
   integrable g (measure.map f μ) ↔ integrable (g ∘ f) μ :=
 f.measurable_embedding.integrable_map_iff
 
+lemma measure_preserving.integrable_comp [opens_measurable_space β] {ν : measure δ} {g : δ → β}
+  {f : α → δ} (hf : measure_preserving f μ ν) (hg : ae_measurable g ν) :
+  integrable (g ∘ f) μ ↔ integrable g ν :=
+by { rw ← hf.map_eq at hg ⊢, exact (integrable_map_measure hg hf.measurable).symm }
+
+lemma measure_preserving.integrable_comp_emb {f : α → δ} {ν} (h₁ : measure_preserving f μ ν)
+  (h₂ : measurable_embedding f) {g : δ → β} :
+  integrable (g ∘ f) μ ↔ integrable g ν :=
+h₁.map_eq ▸ iff.symm h₂.integrable_map_iff
+
 lemma lintegral_edist_lt_top [second_countable_topology β] [opens_measurable_space β] {f g : α → β}
   (hf : integrable f μ) (hg : integrable g μ) :
   ∫⁻ a, edist (f a) (g a) ∂μ < ∞ :=

src/measure_theory/integral/bochner.lean

@@ -1267,6 +1267,11 @@ lemma integral_map_equiv {β} [measurable_space β] (e : α ≃ᵐ β) (f : β 
   ∫ y, f y ∂(measure.map e μ) = ∫ x, f (e x) ∂μ :=
 e.measurable_embedding.integral_map f
 
+lemma measure_preserving.integral_comp {β} {_ : measurable_space β} {f : α → β} {ν}
+  (h₁ : measure_preserving f μ ν) (h₂ : measurable_embedding f) (g : β → E) :
+  ∫ x, g (f x) ∂μ = ∫ y, g y ∂ν :=
+h₁.map_eq ▸ (h₂.integral_map g).symm
+
 @[simp] lemma integral_dirac' [measurable_space α] (f : α → E) (a : α) (hfm : measurable f) :
   ∫ x, f x ∂(measure.dirac a) = f a :=
 calc ∫ x, f x ∂(measure.dirac a) = ∫ x, f a ∂(measure.dirac a) :

src/measure_theory/integral/integrable_on.lean

@@ -181,6 +181,16 @@ lemma integrable_on_map_equiv [measurable_space β] (e : α ≃ᵐ β) {f : β 
   integrable_on f s (measure.map e μ) ↔ integrable_on (f ∘ e) (e ⁻¹' s) μ :=
 by simp only [integrable_on, e.restrict_map, integrable_map_equiv e]
 
+lemma measure_preserving.integrable_on_comp_preimage [measurable_space β] {e : α → β} {ν}
+  (h₁ : measure_preserving e μ ν) (h₂ : measurable_embedding e) {f : β → E} {s : set β} :
+  integrable_on (f ∘ e) (e ⁻¹' s) μ ↔ integrable_on f s ν :=
+(h₁.restrict_preimage_emb h₂ s).integrable_comp_emb h₂
+
+lemma measure_preserving.integrable_on_image [measurable_space β] {e : α → β} {ν}
+  (h₁ : measure_preserving e μ ν) (h₂ : measurable_embedding e) {f : β → E} {s : set α} :
+  integrable_on f (e '' s) ν ↔  integrable_on (f ∘ e) s μ :=
+((h₁.restrict_image_emb h₂ s).integrable_comp_emb h₂).symm
+
 lemma integrable_indicator_iff (hs : measurable_set s) :
   integrable (indicator s f) μ ↔ integrable_on f s μ :=
 by simp [integrable_on, integrable, has_finite_integral, nnnorm_indicator_eq_indicator_nnnorm,