feat(measure_theory/measure/lebesgue): a linear map rescales Lebesgue…

… by the inverse of its determinant (#9195)

Also supporting material to be able to apply Fubini in `ι → ℝ` by separating some coordinates.

src/algebra/big_operators/basic.lean

@@ -259,7 +259,10 @@ namespace finset
 section comm_monoid
 variables [comm_monoid β]
 
-@[to_additive]
+/-- Multiplying the products of a function over `s` and over `sᶜ` gives the whole product.
+For a version expressed with subtypes, see `fintype.prod_subtype_mul_prod_subtype`. -/
+@[to_additive "Adding the sums of a function over `s` and over `sᶜ` gives the whole sum.
+For a version expressed with subtypes, see `fintype.sum_subtype_add_sum_subtype`. "]
 lemma prod_mul_prod_compl [fintype α] [decidable_eq α] (s : finset α) (f : α → β) :
   (∏ i in s, f i) * (∏ i in sᶜ, f i) = ∏ i, f i :=
 is_compl_compl.prod_mul_prod f
@@ -1385,6 +1388,19 @@ begin
   convert prod_unique f
 end
 
+@[to_additive]
+lemma prod_subtype_mul_prod_subtype {α β : Type*} [fintype α] [comm_monoid β]
+  (p : α → Prop) (f : α → β) [decidable_pred p] :
+  (∏ (i : {x // p x}), f i) * (∏ i : {x // ¬ p x}, f i) = ∏ i, f i :=
+begin
+  classical,
+  let s := {x | p x}.to_finset,
+  rw [← finset.prod_subtype s, ← finset.prod_subtype sᶜ],
+  { exact finset.prod_mul_prod_compl _ _ },
+  { simp },
+  { simp }
+end
+
 end fintype
 
 namespace list

src/data/equiv/basic.lean

@@ -1483,6 +1483,28 @@ def subtype_prod_equiv_sigma_subtype {α β : Type*} (p : α → β → Prop) :
   left_inv := λ x, by ext; refl,
   right_inv := λ ⟨a, b, pab⟩, rfl }
 
+/-- The type `Π (i : α), β i` can be split as a product by separating the indices in `α`
+depending on whether they satisfy a predicate `p` or not. -/
+@[simps] def pi_equiv_pi_subtype_prod
+  {α : Type*} (p : α → Prop) (β : α → Type*) [decidable_pred p] :
+  (Π (i : α), β i) ≃ (Π (i : {x // p x}), β i) × (Π (i : {x // ¬ p x}), β i) :=
+{ to_fun := λ f, (λ x, f x, λ x, f x),
+  inv_fun := λ f x, if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩,
+  right_inv := begin
+    rintros ⟨f, g⟩,
+    ext1;
+    { ext y,
+      rcases y,
+      simp only [y_property, dif_pos, dif_neg, not_false_iff, subtype.coe_mk],
+      refl },
+  end,
+  left_inv := λ f, begin
+    ext x,
+    by_cases h : p x;
+    { simp only [h, dif_neg, dif_pos, not_false_iff],
+      refl },
+  end }
+
 end
 
 section subtype_equiv_codomain

src/measure_theory/constructions/pi.lean

@@ -16,6 +16,13 @@ In this file we define and prove properties about finite products of measures
 * `measure_theory.measure.pi`: The product of finitely many σ-finite measures.
   Given `μ : Π i : ι, measure (α i)` for `[fintype ι]` it has type `measure (Π i : ι, α i)`.
 
+To apply Fubini along some subset of the variables, use
+`measure_theory.measure.map_pi_equiv_pi_subtype_prod` to reduce to the situation of a product
+of two measures: this lemma states that the bijection `equiv.pi_equiv_pi_subtype_prod p α`
+between `(Π i : ι, α i)` and `(Π i : {i // p i}, α i) × (Π i : {i // ¬ p i}, α i)` maps a product
+measure to a direct product of product measures, to which one can apply the usual Fubini for
+direct product of measures.
+
 ## Implementation Notes
 
 We define `measure_theory.outer_measure.pi`, the product of finitely many outer measures, as the
@@ -323,7 +330,7 @@ end
 
 variable {μ}
 
-/-- `μ.prod ν` has finite spanning sets in rectangles of finite spanning sets. -/
+/-- `measure.pi μ` has finite spanning sets in rectangles of finite spanning sets. -/
 def finite_spanning_sets_in.pi {C : Π i, set (set (α i))}
   (hμ : ∀ i, (μ i).finite_spanning_sets_in (C i)) (hC : ∀ i (s ∈ C i), measurable_set s) :
   (measure.pi μ).finite_spanning_sets_in (pi univ '' pi univ C) :=
@@ -495,6 +502,46 @@ begin
   exacts [ennreal.prod_lt_top (λ i _, (hμ i).ne), λ i, (ho i).measurable_set]
 end
 
+variable (μ)
+
+/-- Separating the indices into those that satisfy a predicate `p` and those that don't maps
+a product measure to a product of product measures. This is useful to apply Fubini to some subset
+of the variables. The converse is `measure_theory.measure.map_pi_equiv_pi_subtype_prod`. -/
+lemma map_pi_equiv_pi_subtype_prod_symm (p : ι → Prop) [decidable_pred p] :
+  map (equiv.pi_equiv_pi_subtype_prod p α).symm
+    (measure.prod (measure.pi (λ i, μ i)) (measure.pi (λ i, μ i))) = measure.pi μ :=
+begin
+  refine (measure.pi_eq (λ s hs, _)).symm,
+  have A : (equiv.pi_equiv_pi_subtype_prod p α).symm ⁻¹' (set.pi set.univ (λ (i : ι), s i)) =
+    set.prod (set.pi set.univ (λ i, s i)) (set.pi set.univ (λ i, s i)),
+  { ext x,
+    simp only [equiv.pi_equiv_pi_subtype_prod_symm_apply, mem_prod, mem_univ_pi, mem_preimage,
+      subtype.forall],
+    split,
+    { exact λ h, ⟨λ i hi, by simpa [dif_pos hi] using h i,
+                  λ i hi, by simpa [dif_neg hi] using h i⟩ },
+    { assume h i,
+      by_cases hi : p i,
+      { simpa only [dif_pos hi] using h.1 i hi },
+      {simpa only [dif_neg hi] using h.2 i hi } } },
+  rw [measure.map_apply (measurable_pi_equiv_pi_subtype_prod_symm _ p)
+        (measurable_set.univ_pi_fintype hs), A,
+      measure.prod_prod, pi_pi, pi_pi, ← fintype.prod_subtype_mul_prod_subtype p (λ i, μ i (s i))],
+  { exact λ i, hs i.1 },
+  { exact λ i, hs i.1 },
+  { exact measurable_set.univ_pi_fintype (λ i, hs i.1) },
+  { exact measurable_set.univ_pi_fintype (λ i, hs i.1) },
+end
+
+lemma map_pi_equiv_pi_subtype_prod (p : ι → Prop) [decidable_pred p] :
+  map (equiv.pi_equiv_pi_subtype_prod p α) (measure.pi μ) =
+    measure.prod (measure.pi (λ i, μ i)) (measure.pi (λ i, μ i)) :=
+begin
+  rw [← map_pi_equiv_pi_subtype_prod_symm μ p, measure.map_map
+      (measurable_pi_equiv_pi_subtype_prod _ p) (measurable_pi_equiv_pi_subtype_prod_symm _ p)],
+  simp only [equiv.self_comp_symm, map_id]
+end
+
 end measure
 
 instance measure_space.pi [Π i, measure_space (α i)] : measure_space (Π i, α i) :=

src/measure_theory/constructions/prod.lean

@@ -320,6 +320,10 @@ instance prod.measure_space {α β} [measure_space α] [measure_space β] : meas
 
 variables {μ ν} [sigma_finite ν]
 
+lemma volume_eq_prod (α β) [measure_space α] [measure_space β] :
+  (volume : measure (α × β)) = (volume : measure α).prod (volume : measure β) :=
+rfl
+
 lemma prod_apply {s : set (α × β)} (hs : measurable_set s) :
   μ.prod ν s = ∫⁻ x, ν (prod.mk x ⁻¹' s) ∂μ :=
 by simp_rw [measure.prod, bind_apply hs measurable.map_prod_mk_left,

src/measure_theory/measurable_space.lean

@@ -549,6 +549,37 @@ begin
   { simp [measurable_set_pi_of_nonempty hs, h, ← not_nonempty_iff_eq_empty] }
 end
 
+section
+variable (π)
+
+@[measurability]
+lemma measurable_pi_equiv_pi_subtype_prod_symm (p : δ → Prop) [decidable_pred p] :
+  measurable (equiv.pi_equiv_pi_subtype_prod p π).symm :=
+begin
+  apply measurable_pi_iff.2 (λ j, _),
+  by_cases hj : p j,
+  { simp only [hj, dif_pos, equiv.pi_equiv_pi_subtype_prod_symm_apply],
+    have : measurable (λ (f : (Π (i : {x // p x}), π ↑i)), f ⟨j, hj⟩) :=
+      measurable_pi_apply ⟨j, hj⟩,
+    exact measurable.comp this measurable_fst },
+  { simp only [hj, equiv.pi_equiv_pi_subtype_prod_symm_apply, dif_neg, not_false_iff],
+    have : measurable (λ (f : (Π (i : {x // ¬ p x}), π ↑i)), f ⟨j, hj⟩) :=
+      measurable_pi_apply ⟨j, hj⟩,
+    exact measurable.comp this measurable_snd }
+end
+
+@[measurability]
+lemma measurable_pi_equiv_pi_subtype_prod (p : δ → Prop) [decidable_pred p] :
+  measurable (equiv.pi_equiv_pi_subtype_prod p π) :=
+begin
+  refine measurable_prod.2 _,
+  split;
+  { apply measurable_pi_iff.2 (λ j, _),
+    simp only [pi_equiv_pi_subtype_prod_apply, measurable_pi_apply] }
+end
+
+end
+
 section fintype
 
 local attribute [instance] fintype.encodable

src/measure_theory/measure/lebesgue.lean

@@ -5,13 +5,19 @@ Authors: Johannes Hölzl, Yury Kudryashov
 -/
 import measure_theory.constructions.pi
 import measure_theory.measure.stieltjes
+import linear_algebra.matrix.transvection
+import dynamics.ergodic.measure_preserving
+import linear_algebra.determinant
 
 /-!
 # Lebesgue measure on the real line and on `ℝⁿ`
 
 We construct Lebesgue measure on the real line, as a particular case of Stieltjes measure associated
-to the function `x ↦ x`. We obtain as a consequence Lebesgue measure on `ℝⁿ`. We prove their
-basic properties.
+to the function `x ↦ x`. We obtain as a consequence Lebesgue measure on `ℝⁿ`. We prove that they
+are translation invariant.
+
+We show that, on `ℝⁿ`, a linear map acts on Lebesgue measure by rescaling it through the absolute
+value of its determinant, in `real.map_linear_map_volume_pi_eq_smul_volume_pi`.
 -/
 
 noncomputable theory
@@ -208,9 +214,19 @@ lemma map_volume_add_left (a : ℝ) : measure.map ((+) a) volume = volume :=
 eq.symm $ real.measure_ext_Ioo_rat $ λ p q,
   by simp [measure.map_apply (measurable_const_add a) measurable_set_Ioo, sub_sub_sub_cancel_right]
 
+@[simp] lemma volume_preimage_add_left (a : ℝ) (s : set ℝ) : volume (((+) a) ⁻¹' s) = volume s :=
+calc volume (((+) a) ⁻¹' s) = measure.map ((+) a) volume s :
+  ((homeomorph.add_left a).to_measurable_equiv.map_apply s).symm
+... = volume s : by rw map_volume_add_left
+
 lemma map_volume_add_right (a : ℝ) : measure.map (+ a) volume = volume :=
 by simpa only [add_comm] using real.map_volume_add_left a
 
+@[simp] lemma volume_preimage_add_right (a : ℝ) (s : set ℝ) : volume ((+ a) ⁻¹' s) = volume s :=
+calc volume ((+ a) ⁻¹' s) = measure.map (+ a) volume s :
+  ((homeomorph.add_right a).to_measurable_equiv.map_apply s).symm
+... = volume s : by rw map_volume_add_right
+
 lemma smul_map_volume_mul_left {a : ℝ} (h : a ≠ 0) :
   ennreal.of_real (abs a) • measure.map ((*) a) volume = volume :=
 begin
@@ -231,6 +247,12 @@ by conv_rhs { rw [← real.smul_map_volume_mul_left h, smul_smul,
   ← ennreal.of_real_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel h, abs_one, ennreal.of_real_one,
   one_smul] }
 
+@[simp] lemma volume_preimage_mul_left {a : ℝ} (h : a ≠ 0) (s : set ℝ) :
+  volume (((*) a) ⁻¹' s) = ennreal.of_real (abs a⁻¹) * volume s :=
+calc volume (((*) a) ⁻¹' s) = measure.map ((*) a) volume s :
+  ((homeomorph.mul_left' a h).to_measurable_equiv.map_apply s).symm
+... = ennreal.of_real (abs a⁻¹) * volume s : by { rw map_volume_mul_left h, refl }
+
 lemma smul_map_volume_mul_right {a : ℝ} (h : a ≠ 0) :
   ennreal.of_real (abs a) • measure.map (* a) volume = volume :=
 by simpa only [mul_comm] using real.smul_map_volume_mul_left h
@@ -239,11 +261,152 @@ lemma map_volume_mul_right {a : ℝ} (h : a ≠ 0) :
   measure.map (* a) volume = ennreal.of_real (abs a⁻¹) • volume :=
 by simpa only [mul_comm] using real.map_volume_mul_left h
 
+@[simp] lemma volume_preimage_mul_right {a : ℝ} (h : a ≠ 0) (s : set ℝ) :
+  volume ((* a) ⁻¹' s) = ennreal.of_real (abs a⁻¹) * volume s :=
+calc volume ((* a) ⁻¹' s) = measure.map (* a) volume s :
+  ((homeomorph.mul_right' a h).to_measurable_equiv.map_apply s).symm
+... = ennreal.of_real (abs a⁻¹) * volume s : by { rw map_volume_mul_right h, refl }
+
 @[simp] lemma map_volume_neg : measure.map has_neg.neg (volume : measure ℝ) = volume :=
 eq.symm $ real.measure_ext_Ioo_rat $ λ p q,
   by simp [show measure.map has_neg.neg volume (Ioo (p : ℝ) q) = _,
     from measure.map_apply measurable_neg measurable_set_Ioo]
 
+/-!
+### Images of the Lebesgue measure under translation/linear maps in ℝⁿ
+-/
+
+lemma map_volume_pi_add_left (a : ι → ℝ) : measure.map ((+) a) volume = volume :=
+begin
+  refine (measure.pi_eq (λ s hs, _)).symm,
+  have A : has_add.add a ⁻¹' (set.pi univ (λ (i : ι), s i))
+    = set.pi univ (λ (i : ι), ((+) (a i)) ⁻¹' (s i)), by { ext, simp },
+  rw [measure.map_apply (measurable_const_add a) (measurable_set.univ_pi_fintype hs), A,
+      volume_pi_pi],
+  { simp only [volume_preimage_add_left] },
+  { exact λ i, measurable_const_add (a i) (hs i) }
+end
+
+@[simp] lemma volume_pi_preimage_add_left (a : ι → ℝ) (s : set (ι → ℝ)) :
+  volume (((+) a) ⁻¹' s) = volume s :=
+calc volume (((+) a) ⁻¹' s) = measure.map ((+) a) volume s :
+  ((homeomorph.add_left a).to_measurable_equiv.map_apply s).symm
+... = volume s : by rw map_volume_pi_add_left
+
+open matrix
+
+/-- A diagonal matrix rescales Lebesgue according to its determinant. This is a special case of
+`real.map_matrix_volume_pi_eq_smul_volume_pi`, that one should use instead (and whose proof
+uses this particular case). -/
+lemma smul_map_diagonal_volume_pi [decidable_eq ι] {D : ι → ℝ} (h : det (diagonal D) ≠ 0) :
+  ennreal.of_real (abs (det (diagonal D))) • measure.map ((diagonal D).to_lin') volume = volume :=
+begin
+  refine (measure.pi_eq (λ s hs, _)).symm,
+  simp only [det_diagonal, measure.coe_smul, algebra.id.smul_eq_mul, pi.smul_apply],
+  rw [measure.map_apply _ (measurable_set.univ_pi_fintype hs)],
+  swap, { exact continuous.measurable (linear_map.continuous_on_pi _) },
+  have : (matrix.to_lin' (diagonal D)) ⁻¹' (set.pi set.univ (λ (i : ι), s i))
+    = set.pi set.univ (λ (i : ι), ((*) (D i)) ⁻¹' (s i)),
+  { ext f,
+    simp only [linear_map.coe_proj, algebra.id.smul_eq_mul, linear_map.smul_apply, mem_univ_pi,
+      mem_preimage, linear_map.pi_apply, diagonal_to_lin'] },
+  have B : ∀ i, of_real (abs (D i)) * volume (has_mul.mul (D i) ⁻¹' s i) = volume (s i),
+  { assume i,
+    have A : D i ≠ 0,
+    { simp only [det_diagonal, ne.def] at h,
+      exact finset.prod_ne_zero_iff.1 h i (finset.mem_univ i) },
+    rw [volume_preimage_mul_left A, ← mul_assoc, ← ennreal.of_real_mul (abs_nonneg _), ← abs_mul,
+      mul_inv_cancel A, abs_one, ennreal.of_real_one, one_mul] },
+  rw [this, volume_pi_pi, finset.abs_prod,
+    ennreal.of_real_prod_of_nonneg (λ i hi, abs_nonneg (D i)), ← finset.prod_mul_distrib],
+  { simp only [B] },
+  { exact λ i, measurable_const_mul _ (hs i) },
+end
+
+/-- A transvection preserves Lebesgue measure. -/
+lemma map_transvection_volume_pi [decidable_eq ι] (t : transvection_struct ι ℝ) :
+  measure.map (t.to_matrix.to_lin') volume = volume :=
+begin
+  /- We separate the coordinate along which there is a shearing from the other ones, and apply
+  Fubini. Along this coordinate (and when all the other coordinates are fixed), it acts like a
+  translation, and therefore preserves Lebesgue. -/
+  suffices H : measure_preserving t.to_matrix.to_lin' volume volume, by exact H.2,
+  let p : ι → Prop := λ i, i ≠ t.i,
+  let α : Type* := {x // p x},
+  let β : Type* := {x // ¬ (p x)},
+  let g : (α → ℝ) → (β → ℝ) → (β → ℝ) := λ a b, (λ x, t.c * a ⟨t.j, t.hij.symm⟩) + b,
+  let F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) :=
+    λ p, (id p.1, g p.1 p.2),
+  let e := equiv.pi_equiv_pi_subtype_prod p (λ (i : ι), ℝ),
+  have : (t.to_matrix.to_lin' : (ι → ℝ) → (ι → ℝ)) = e.symm ∘ F ∘ e,
+  { cases t,
+    ext f k,
+    simp only [linear_equiv.map_smul, dite_eq_ite, linear_map.id_coe, p, ite_not,
+      algebra.id.smul_eq_mul, one_mul, dot_product, std_basis_matrix,
+      equiv.pi_equiv_pi_subtype_prod_symm_apply, id.def, transvection,
+      pi.add_apply, zero_mul, linear_map.smul_apply, function.comp_app,
+      equiv.pi_equiv_pi_subtype_prod_apply, matrix.transvection_struct.to_matrix_mk,
+      matrix.mul_vec, linear_equiv.map_add, ite_mul, e, matrix.to_lin'_apply,
+      pi.smul_apply, subtype.coe_mk, g, linear_map.add_apply, finset.sum_congr, matrix.to_lin'_one],
+    by_cases h : t_i = k,
+    { simp only [h, true_and, finset.mem_univ, if_true, eq_self_iff_true, finset.sum_ite_eq,
+        one_apply, boole_mul, add_comm], },
+    { simp only [h, ne.symm h, add_zero, if_false, finset.sum_const_zero, false_and, mul_zero] } },
+  rw this,
+  have A : measure_preserving e volume volume :=
+  ⟨ measurable_pi_equiv_pi_subtype_prod (λ i, ℝ) _,
+    (measure.map_pi_equiv_pi_subtype_prod (λ i, (volume : measure ℝ)) p : _) ⟩,
+  have B : measure_preserving F volume volume,
+  { have g_meas : measurable (function.uncurry g),
+    { have : measurable (λ (c : (α → ℝ)), c ⟨t.j, t.hij.symm⟩) :=
+        measurable_pi_apply ⟨t.j, t.hij.symm⟩,
+      refine measurable.add (measurable_pi_lambda _ (λ i, measurable.const_mul _ _)) measurable_snd,
+      exact this.comp measurable_fst },
+    exact measure_preserving.skew_product (measure_preserving.id _) g_meas
+      (eventually_of_forall (λ a, map_volume_pi_add_left _)) },
+  have C : measure_preserving e.symm volume volume :=
+  ⟨ (measurable_pi_equiv_pi_subtype_prod_symm (λ (i : ι), ℝ) p : _),
+    (measure.map_pi_equiv_pi_subtype_prod_symm (λ (i : ι), volume) p : _) ⟩,
+  exact (C.comp B).comp A,
+end
+
+/-- Any invertible matrix rescales Lebesgue measure through the absolute value of its
+determinant. -/
+lemma map_matrix_volume_pi_eq_smul_volume_pi [decidable_eq ι] {M : matrix ι ι ℝ} (hM : det M ≠ 0) :
+  measure.map (M.to_lin') volume = ennreal.of_real (abs (det M)⁻¹) • volume :=
+begin
+  -- This follows from the cases we have already proved, of diagonal matrices and transvections,
+  -- as these matrices generate all invertible matrices.
+  apply diagonal_transvection_induction_of_det_ne_zero _ M hM (λ D hD, _) (λ t, _)
+    (λ A B hA hB IHA IHB, _),
+  { conv_rhs { rw [← smul_map_diagonal_volume_pi hD] },
+    rw [smul_smul, ← ennreal.of_real_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel hD, abs_one,
+      ennreal.of_real_one, one_smul] },
+  { simp only [matrix.transvection_struct.det, ennreal.of_real_one, map_transvection_volume_pi,
+      one_smul, _root_.inv_one, abs_one] },
+  { rw [to_lin'_mul, det_mul, linear_map.coe_comp, ← measure.map_map, IHB, linear_map.map_smul,
+      IHA, smul_smul, ← ennreal.of_real_mul (abs_nonneg _), ← abs_mul, mul_comm, mul_inv'],
+    { apply continuous.measurable,
+      apply linear_map.continuous_on_pi },
+    { apply continuous.measurable,
+      apply linear_map.continuous_on_pi } }
+end
+
+/-- Any invertible linear map rescales Lebesgue measure through the absolute value of its
+determinant. -/
+lemma map_linear_map_volume_pi_eq_smul_volume_pi {f : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)} (hf : f.det ≠ 0) :
+  measure.map f volume = ennreal.of_real (abs (f.det)⁻¹) • volume :=
+begin
+  -- this is deduced from the matrix case
+  classical,
+  let M := f.to_matrix',
+  have A : f.det = det M, by simp only [linear_map.det_to_matrix'],
+  have B : f = M.to_lin', by simp only [to_lin'_to_matrix'],
+  rw [A, B],
+  apply map_matrix_volume_pi_eq_smul_volume_pi,
+  rwa A at hf
+end
+
 end real
 
 open_locale topological_space