feat(measure_theory/measure/haar_lebesgue): Lebesgue measure of the i…

…mage of a set under a linear map (#11038)

The image of a set `s` under a linear map `f` has measure equal to `μ s` times the absolute value of the determinant of `f`.

src/measure_theory/measure/haar_lebesgue.lean

@@ -17,6 +17,12 @@ We prove that the Haar measure and Lebesgue measure are equal on `ℝ` and on `
 We deduce basic properties of any Haar measure on a finite dimensional real vector space:
 * `map_linear_map_add_haar_eq_smul_add_haar`: a linear map rescales the Haar measure by the
   absolute value of its determinant.
+* `add_haar_preimage_linear_map` : when `f` is a linear map with nonzero determinant, the measure
+  of `f ⁻¹' s` is the measure of `s` multiplied by the absolute value of the inverse of the
+  determinant of `f`.
+* `add_haar_image_linear_map` :  when `f` is a linear map, the measure of `f '' s` is the
+  measure of `s` multiplied by the absolute value of the determinant of `f`.
+* `add_haar_submodule` : a strict submodule has measure `0`.
 * `add_haar_smul` : the measure of `r • s` is `|r| ^ dim * μ s`.
 * `add_haar_ball`: the measure of `ball x r` is `r ^ dim * μ (ball 0 1)`.
 * `add_haar_closed_ball`: the measure of `closed_ball x r` is `r ^ dim * μ (ball 0 1)`.
@@ -84,6 +90,89 @@ by { rw ← add_haar_measure_eq_volume_pi, apply_instance }
 
 namespace measure
 
+/-!
+### Strict subspaces have zero measure
+-/
+
+/-- If a set is disjoint of its translates by infinitely many bounded vectors, then it has measure
+zero. This auxiliary lemma proves this assuming additionally that the set is bounded. -/
+lemma add_haar_eq_zero_of_disjoint_translates_aux
+  {E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
+  [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ]
+  {s : set E} (u : ℕ → E) (sb : bounded s) (hu : bounded (range u))
+  (hs : pairwise (disjoint on (λ n, {u n} + s))) (h's : measurable_set s) :
+  μ s = 0 :=
+begin
+  by_contra h,
+  apply lt_irrefl ∞,
+  calc
+  ∞ = ∑' (n : ℕ), μ s : (ennreal.tsum_const_eq_top_of_ne_zero h).symm
+  ... = ∑' (n : ℕ), μ ({u n} + s) :
+    by { congr' 1, ext1 n, simp only [image_add_left, add_haar_preimage_add, singleton_add] }
+  ... = μ (⋃ n, {u n} + s) :
+    by rw measure_Union hs
+      (λ n, by simpa only [image_add_left, singleton_add] using measurable_id.const_add _ h's)
+  ... = μ (range u + s) : by rw [← Union_add, Union_singleton_eq_range]
+  ... < ∞ : bounded.measure_lt_top (hu.add sb)
+end
+
+/-- If a set is disjoint of its translates by infinitely many bounded vectors, then it has measure
+zero. -/
+lemma add_haar_eq_zero_of_disjoint_translates
+  {E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
+  [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ]
+  {s : set E} (u : ℕ → E) (hu : bounded (range u))
+  (hs : pairwise (disjoint on (λ n, {u n} + s))) (h's : measurable_set s) :
+  μ s = 0 :=
+begin
+  suffices H : ∀ R, μ (s ∩ closed_ball 0 R) = 0,
+  { apply le_antisymm _ (zero_le _),
+    have : s ⊆ ⋃ (n : ℕ), s ∩ closed_ball 0 n,
+    { assume x hx,
+      obtain ⟨n, hn⟩ : ∃ (n : ℕ), ∥x∥ ≤ n := exists_nat_ge (∥x∥),
+      exact mem_Union.2 ⟨n, ⟨hx, mem_closed_ball_zero_iff.2 hn⟩⟩ },
+    calc μ s ≤ μ (⋃ (n : ℕ), s ∩ closed_ball 0 n) : measure_mono this
+    ... ≤ ∑' (n : ℕ), μ (s ∩ closed_ball 0 n) : measure_Union_le _
+    ... = 0 : by simp only [H, tsum_zero] },
+  assume R,
+  apply add_haar_eq_zero_of_disjoint_translates_aux μ u
+    (bounded.mono (inter_subset_right _ _) bounded_closed_ball) hu _
+    (h's.inter (measurable_set_closed_ball)),
+  rw ← pairwise_univ at ⊢ hs,
+  apply pairwise_disjoint.mono hs (λ n, _),
+  exact add_subset_add (subset.refl _) (inter_subset_left _ _)
+end
+
+/-- A strict vector subspace has measure zero. -/
+lemma add_haar_submodule
+  {E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
+  [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ]
+  (s : submodule ℝ E) (hs : s ≠ ⊤) : μ s = 0 :=
+begin
+  obtain ⟨x, hx⟩ : ∃ x, x ∉ s,
+    by simpa only [submodule.eq_top_iff', not_exists, ne.def, not_forall] using hs,
+  obtain ⟨c, cpos, cone⟩ : ∃ (c : ℝ), 0 < c ∧ c < 1 := ⟨1/2, by norm_num, by norm_num⟩,
+  have A : bounded (range (λ (n : ℕ), (c ^ n) • x)),
+  { have : tendsto (λ (n : ℕ), (c ^ n) • x) at_top (𝓝 ((0 : ℝ) • x)) :=
+      (tendsto_pow_at_top_nhds_0_of_lt_1 cpos.le cone).smul_const x,
+    exact bounded_range_of_tendsto _ this },
+  apply add_haar_eq_zero_of_disjoint_translates μ _ A _
+    (submodule.closed_of_finite_dimensional s).measurable_set,
+  assume m n hmn,
+  simp only [function.on_fun, image_add_left, singleton_add, disjoint_left, mem_preimage,
+             set_like.mem_coe],
+  assume y hym hyn,
+  have A : (c ^ n - c ^ m) • x ∈ s,
+  { convert s.sub_mem hym hyn,
+    simp only [sub_smul, neg_sub_neg, add_sub_add_right_eq_sub] },
+  have H : c ^ n - c ^ m ≠ 0,
+    by simpa only [sub_eq_zero, ne.def] using (strict_anti_pow cpos cone).injective.ne hmn.symm,
+  have : x ∈ s,
+  { convert s.smul_mem (c ^ n - c ^ m)⁻¹ A,
+    rw [smul_smul, inv_mul_cancel H, one_smul] },
+  exact hx this
+end
+
 /-!
 ### Applying a linear map rescales Haar measure by the determinant
 
@@ -101,7 +190,7 @@ begin
   /- We have already proved the result for the Lebesgue product measure, using matrices.
   We deduce it for any Haar measure by uniqueness (up to scalar multiplication). -/
   have := add_haar_measure_unique (is_add_left_invariant_add_haar μ) (pi_Icc01 ι),
-  conv_lhs { rw this }, conv_rhs { rw this },
+  rw this,
   simp [add_haar_measure_eq_volume_pi, real.map_linear_map_volume_pi_eq_smul_volume_pi hf,
     smul_smul, mul_comm],
 end
@@ -113,7 +202,7 @@ lemma map_linear_map_add_haar_eq_smul_add_haar
   measure.map f μ = ennreal.of_real (abs (f.det)⁻¹) • μ :=
 begin
   -- we reduce to the case of `E = ι → ℝ`, for which we have already proved the result using
-  -- matrices in `map_linear_map_haar_pi_eq_smul_haar`.
+  -- matrices in `map_linear_map_add_haar_pi_eq_smul_add_haar`.
   let ι := fin (finrank ℝ E),
   haveI : finite_dimensional ℝ (ι → ℝ) := by apply_instance,
   have : finrank ℝ E = finrank ℝ (ι → ℝ), by simp,
@@ -139,7 +228,9 @@ begin
     map_map Cesymm.measurable Ce.measurable, ecomp, measure.map_id]
 end
 
-@[simp] lemma haar_preimage_linear_map
+/-- The preimage of a set `s` under a linear map `f` with nonzero determinant has measure
+equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
+@[simp] lemma add_haar_preimage_linear_map
   {E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
   [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ]
   {f : E →ₗ[ℝ] E} (hf : f.det ≠ 0) (s : set E) :
@@ -150,6 +241,78 @@ calc μ (f ⁻¹' s) = measure.map f μ s :
 ... = ennreal.of_real (abs (f.det)⁻¹) * μ s :
   by { rw map_linear_map_add_haar_eq_smul_add_haar μ hf, refl }
 
+/-- The preimage of a set `s` under a continuous linear map `f` with nonzero determinant has measure
+equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
+@[simp] lemma add_haar_preimage_continuous_linear_map
+  {E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
+  [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ]
+  {f : E →L[ℝ] E} (hf : linear_map.det (f : E →ₗ[ℝ] E) ≠ 0) (s : set E) :
+  μ (f ⁻¹' s) = ennreal.of_real (abs (linear_map.det (f : E →ₗ[ℝ] E))⁻¹) * μ s :=
+add_haar_preimage_linear_map μ hf s
+
+/-- The preimage of a set `s` under a linear equiv `f` has measure
+equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
+@[simp] lemma add_haar_preimage_linear_equiv
+  {E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
+  [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ]
+  (f : E ≃ₗ[ℝ] E) (s : set E) :
+  μ (f ⁻¹' s) = ennreal.of_real (abs (f.symm : E →ₗ[ℝ] E).det) * μ s :=
+begin
+  have A : (f : E →ₗ[ℝ] E).det ≠ 0 := (linear_equiv.is_unit_det' f).ne_zero,
+  convert add_haar_preimage_linear_map μ A s,
+  simp only [linear_equiv.det_coe_symm]
+end
+
+/-- The preimage of a set `s` under a continuous linear equiv `f` has measure
+equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
+@[simp] lemma add_haar_preimage_continuous_linear_equiv
+  {E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
+  [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ]
+  (f : E ≃L[ℝ] E) (s : set E) :
+  μ (f ⁻¹' s) = ennreal.of_real (abs (f.symm : E →ₗ[ℝ] E).det) * μ s :=
+add_haar_preimage_linear_equiv μ _ s
+
+/-- The image of a set `s` under a linear map `f` has measure
+equal to `μ s` times the absolute value of the determinant of `f`. -/
+@[simp] lemma add_haar_image_linear_map
+  {E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
+  [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ]
+  (f : E →ₗ[ℝ] E) (s : set E) :
+  μ (f '' s) = ennreal.of_real (abs f.det) * μ s :=
+begin
+  rcases ne_or_eq f.det 0 with hf|hf,
+  { let g := (f.equiv_of_det_ne_zero hf).to_continuous_linear_equiv,
+    change μ (g '' s) = _,
+    rw [continuous_linear_equiv.image_eq_preimage g s, add_haar_preimage_continuous_linear_equiv],
+    congr,
+    ext x,
+    simp only [linear_equiv.of_is_unit_det_apply, linear_equiv.to_continuous_linear_equiv_apply,
+      continuous_linear_equiv.symm_symm, continuous_linear_equiv.coe_coe,
+      continuous_linear_map.coe_coe, linear_equiv.to_fun_eq_coe, coe_coe] },
+  { simp only [hf, zero_mul, ennreal.of_real_zero, abs_zero],
+    have : μ f.range = 0 :=
+      add_haar_submodule μ _ (linear_map.range_lt_top_of_det_eq_zero hf).ne,
+    exact le_antisymm (le_trans (measure_mono (image_subset_range _ _)) this.le) (zero_le _) }
+end
+
+/-- The image of a set `s` under a continuous linear map `f` has measure
+equal to `μ s` times the absolute value of the determinant of `f`. -/
+@[simp] lemma add_haar_image_continuous_linear_map
+  {E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
+  [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ]
+  (f : E →L[ℝ] E) (s : set E) :
+  μ (f '' s) = ennreal.of_real (abs (f : E →ₗ[ℝ] E).det) * μ s :=
+add_haar_image_linear_map μ _ s
+
+/-- The image of a set `s` under a continuous linear equiv `f` has measure
+equal to `μ s` times the absolute value of the determinant of `f`. -/
+@[simp] lemma add_haar_image_continuous_linear_equiv
+  {E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
+  [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ]
+  (f : E ≃L[ℝ] E) (s : set E) :
+  μ (f '' s) = ennreal.of_real (abs (f : E →ₗ[ℝ] E).det) * μ s :=
+add_haar_image_linear_map μ _ s
+
 /-!
 ### Basic properties of Haar measures on real vector spaces
 -/
@@ -170,14 +333,14 @@ begin
     monoid_hom.map_one],
 end
 
-lemma add_haar_preimage_smul {r : ℝ} (hr : r ≠ 0) (s : set E) :
+@[simp] lemma add_haar_preimage_smul {r : ℝ} (hr : r ≠ 0) (s : set E) :
   μ (((•) r) ⁻¹' s) = ennreal.of_real (abs (r ^ (finrank ℝ E))⁻¹) * μ s :=
 calc μ (((•) r) ⁻¹' s) = measure.map ((•) r) μ s :
   ((homeomorph.smul (is_unit_iff_ne_zero.2 hr).unit).to_measurable_equiv.map_apply s).symm
 ... = ennreal.of_real (abs (r^(finrank ℝ E))⁻¹) * μ s : by { rw map_add_haar_smul μ hr, refl }
 
 /-- Rescaling a set by a factor `r` multiplies its measure by `abs (r ^ dim)`. -/
-lemma add_haar_smul (r : ℝ) (s : set E) :
+@[simp] lemma add_haar_smul (r : ℝ) (s : set E) :
   μ (r • s) = ennreal.of_real (abs (r ^ (finrank ℝ E))) * μ s :=
 begin
   rcases ne_or_eq r 0 with h|rfl,