feat(measure_theory/measure/haar_lebesgue): measure of an affine subs…

…pace is zero (#13137)

* Additive Haar measure of an affine subspace of a finite dimensional
real vector space is zero.

* Additive Haar measure of the image of a set `s` under `homothety x r` is
  equal to `|r ^ d| * μ s`.

src/linear_algebra/affine_space/affine_subspace.lean

@@ -752,6 +752,18 @@ by rw [direction_eq_vector_span, bot_coe, vector_span_def, vsub_empty, submodule
 
 variables {k V P}
 
+@[simp] lemma coe_eq_bot_iff (Q : affine_subspace k P) : (Q : set P) = ∅ ↔ Q = ⊥ :=
+coe_injective.eq_iff' (bot_coe _ _ _)
+
+@[simp] lemma coe_eq_univ_iff (Q : affine_subspace k P) : (Q : set P) = univ ↔ Q = ⊤ :=
+coe_injective.eq_iff' (top_coe _ _ _)
+
+lemma nonempty_iff_ne_bot (Q : affine_subspace k P) : (Q : set P).nonempty ↔ Q ≠ ⊥ :=
+by { rw ← ne_empty_iff_nonempty, exact not_congr Q.coe_eq_bot_iff }
+
+lemma eq_bot_or_nonempty (Q : affine_subspace k P) : Q = ⊥ ∨ (Q : set P).nonempty :=
+by { rw nonempty_iff_ne_bot, apply eq_or_ne }
+
 lemma subsingleton_of_subsingleton_span_eq_top {s : set P} (h₁ : s.subsingleton)
   (h₂ : affine_span k s = ⊤) : subsingleton P :=
 begin

src/measure_theory/measure/haar_lebesgue.lean

@@ -163,6 +163,21 @@ begin
   exact hx this
 end
 
+/-- A strict affine subspace has measure zero. -/
+lemma add_haar_affine_subspace
+  {E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
+  [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ]
+  (s : affine_subspace ℝ E) (hs : s ≠ ⊤) : μ s = 0 :=
+begin
+  rcases s.eq_bot_or_nonempty with rfl|hne,
+  { rw [affine_subspace.bot_coe, measure_empty] },
+  rw [ne.def, ← affine_subspace.direction_eq_top_iff_of_nonempty hne] at hs,
+  rcases hne with ⟨x, hx : x ∈ s⟩,
+  simpa only [affine_subspace.coe_direction_eq_vsub_set_right hx, vsub_eq_sub,
+    sub_eq_add_neg, image_add_right, neg_neg, measure_preimage_add_right]
+    using add_haar_submodule μ s.direction hs
+end
+
 /-!
 ### Applying a linear map rescales Haar measure by the determinant
 
@@ -346,6 +361,13 @@ begin
       measure_singleton] }
 end
 
+@[simp] lemma add_haar_image_homothety (x : E) (r : ℝ) (s : set E) :
+  μ (affine_map.homothety x r '' s) = ennreal.of_real (abs (r ^ (finrank ℝ E))) * μ s :=
+calc μ (affine_map.homothety x r '' s) = μ ((λ y, y + x) '' (r • ((λ y, y + (-x)) '' s))) :
+  by { simp only [← image_smul, image_image, ← sub_eq_add_neg], refl }
+... = ennreal.of_real (abs (r ^ (finrank ℝ E))) * μ s :
+  by simp only [image_add_right, measure_preimage_add_right, add_haar_smul]
+
 /-! We don't need to state `map_add_haar_neg` here, because it has already been proved for
 general Haar measures on general commutative groups. -/