refactor(measure_theory/measure/lebesgue): use ‖a‖₊ • instead of ennreal.of_real (|a|) *

src/data/real/ennreal.lean

@@ -1738,6 +1738,11 @@ lemma of_real_nsmul {x : ℝ} {n : ℕ} :
   ennreal.of_real (n • x) = n • ennreal.of_real x :=
 by simp only [nsmul_eq_mul, ← of_real_coe_nat n, ← of_real_mul n.cast_nonneg]
 
+lemma of_real_nnreal_smul (c : ℝ≥0) (x : ℝ) :
+  ennreal.of_real (c • x) = c • ennreal.of_real x :=
+by simp_rw [nnreal.smul_def, smul_eq_mul, of_real_mul c.coe_nonneg, of_real_coe_nnreal, smul_def,
+  smul_eq_mul]
+
 lemma of_real_inv_of_pos {x : ℝ} (hx : 0 < x) :
   (ennreal.of_real x)⁻¹ = ennreal.of_real x⁻¹ :=
 by rw [ennreal.of_real, ennreal.of_real, ←@coe_inv (real.to_nnreal x) (by simp [hx]), coe_eq_coe,

src/measure_theory/measure/lebesgue/basic.lean

@@ -244,44 +244,42 @@ calc volume s ≤ ∏ i : ι, emetric.diam (function.eval i '' s) : volume_pi_le
 -/
 
 lemma smul_map_volume_mul_left {a : ℝ} (h : a ≠ 0) :
-  ennreal.of_real (|a|) • measure.map ((*) a) volume = volume :=
+  ‖a‖₊ • measure.map ((*) a) volume = volume :=
 begin
   refine (real.measure_ext_Ioo_rat $ λ p q, _).symm,
+  rw [measure.smul_apply, measure.map_apply (measurable_const_mul a) measurable_set_Ioo],
   cases lt_or_gt_of_ne h with h h,
-  { simp only [real.volume_Ioo, measure.smul_apply, ← ennreal.of_real_mul (le_of_lt $ neg_pos.2 h),
-      measure.map_apply (measurable_const_mul a) measurable_set_Ioo, neg_sub_neg,
-      neg_mul, preimage_const_mul_Ioo_of_neg _ _ h, abs_of_neg h, mul_sub, smul_eq_mul,
-      mul_div_cancel' _ (ne_of_lt h)] },
-  { simp only [real.volume_Ioo, measure.smul_apply, ← ennreal.of_real_mul (le_of_lt h),
-      measure.map_apply (measurable_const_mul a) measurable_set_Ioo, preimage_const_mul_Ioo _ _ h,
-      abs_of_pos h, mul_sub, mul_div_cancel' _ (ne_of_gt h), smul_eq_mul] }
+  { simp_rw [preimage_const_mul_Ioo_of_neg _ _ h, real.volume_Ioo, ←ennreal.of_real_nnreal_smul,
+      nnreal.smul_def, coe_nnnorm, smul_eq_mul, norm_eq_abs, abs_of_neg h, mul_sub, neg_mul,
+      neg_sub_neg, mul_div_cancel' _ (ne_of_lt h)] },
+  { simp_rw [preimage_const_mul_Ioo _ _ h, real.volume_Ioo, ←ennreal.of_real_nnreal_smul,
+      nnreal.smul_def, coe_nnnorm, smul_eq_mul, norm_eq_abs, abs_of_pos h, mul_sub,
+      mul_div_cancel' _ (ne_of_gt h)] }
 end
 
 lemma map_volume_mul_left {a : ℝ} (h : a ≠ 0) :
-  measure.map ((*) a) volume = ennreal.of_real (|a⁻¹|) • volume :=
-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] }
+  measure.map ((*) a) volume = ‖a⁻¹‖₊ • volume :=
+by rw [nnnorm_inv, eq_inv_smul_iff₀ (nnnorm_ne_zero_iff.mpr h), smul_map_volume_mul_left h]
 
 @[simp] lemma volume_preimage_mul_left {a : ℝ} (h : a ≠ 0) (s : set ℝ) :
-  volume (((*) a) ⁻¹' s) = ennreal.of_real (abs a⁻¹) * volume s :=
+  volume (((*) a) ⁻¹' s) = ‖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 }
+... = ‖a⁻¹‖₊ * volume s : by { rw map_volume_mul_left h, refl }
 
 lemma smul_map_volume_mul_right {a : ℝ} (h : a ≠ 0) :
-  ennreal.of_real (|a|) • measure.map (* a) volume = volume :=
+  ‖a‖₊ • measure.map (* a) volume = volume :=
 by simpa only [mul_comm] using real.smul_map_volume_mul_left h
 
 lemma map_volume_mul_right {a : ℝ} (h : a ≠ 0) :
-  measure.map (* a) volume = ennreal.of_real (|a⁻¹|) • volume :=
+  measure.map (* a) volume = ‖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 :=
+  volume ((* a) ⁻¹' s) = ‖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 }
+... = ‖a⁻¹‖₊ • volume s : by { rw map_volume_mul_right h, refl }
 
 /-!
 ### Images of the Lebesgue measure under translation/linear maps in ℝⁿ
@@ -293,7 +291,7 @@ open matrix
 `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 :=
+  ‖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],
@@ -304,16 +302,15 @@ begin
   { 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),
+  have B : ∀ i, ‖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]
+    rw [volume_preimage_mul_left A, nnnorm_inv, smul_inv_smul₀ (nnnorm_ne_zero_iff.mpr A)] },
+  simp_rw [this, volume_pi_pi, nnnorm_prod, ennreal.smul_def, smul_eq_mul, ennreal.coe_finset_prod,
+    ← finset.prod_mul_distrib, ←smul_eq_mul, ←ennreal.smul_def],
+  simp only [B],
 end
 
 /-- A transvection preserves Lebesgue measure. -/
@@ -361,19 +358,18 @@ 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 :=
+  measure.map M.to_lin' volume = ‖(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] },
+    rw [nnnorm_inv, inv_smul_smul₀ (nnnorm_ne_zero_iff.mpr hD)] },
   { simp only [matrix.transvection_struct.det, ennreal.of_real_one,
-      (volume_preserving_transvection_struct _).map_eq, one_smul, _root_.inv_one, abs_one] },
-  { rw [to_lin'_mul, det_mul, linear_map.coe_comp, ← measure.map_map, IHB, measure.map_smul,
-      IHA, smul_smul, ← ennreal.of_real_mul (abs_nonneg _), ← abs_mul, mul_comm, mul_inv],
+      (volume_preserving_transvection_struct _).map_eq, one_smul, _root_.inv_one, nnnorm_one] },
+  { rw [to_lin'_mul, det_mul, linear_map.coe_comp, ← measure.map_map, IHB, measure.map_smul_nnreal,
+      IHA, smul_smul, ← nnnorm_mul, _root_.mul_inv_rev],
     { apply continuous.measurable,
       apply linear_map.continuous_on_pi },
     { apply continuous.measurable,
@@ -383,7 +379,7 @@ 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 :=
+  measure.map f volume = ‖f.det⁻¹‖₊ • volume :=
 begin
   -- this is deduced from the matrix case
   classical,

src/measure_theory/measure/lebesgue/eq_haar.lean

@@ -207,7 +207,7 @@ linear equiv maps Haar measure to Haar measure.
 lemma map_linear_map_add_haar_pi_eq_smul_add_haar
   {ι : Type*} [finite ι] {f : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)} (hf : f.det ≠ 0)
   (μ : measure (ι → ℝ)) [is_add_haar_measure μ] :
-  measure.map f μ = ennreal.of_real (abs (f.det)⁻¹) • μ :=
+  measure.map f μ = ‖(f.det)⁻¹‖₊ • μ :=
 begin
   casesI nonempty_fintype ι,
   /- We have already proved the result for the Lebesgue product measure, using matrices.
@@ -223,7 +223,7 @@ variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [measurable
 
 lemma map_linear_map_add_haar_eq_smul_add_haar
   {f : E →ₗ[ℝ] E} (hf : f.det ≠ 0) :
-  measure.map f μ = ennreal.of_real (abs (f.det)⁻¹) • μ :=
+  measure.map f μ = ‖(f.det)⁻¹‖₊ • μ :=
 begin
   -- we reduce to the case of `E = ι → ℝ`, for which we have already proved the result using
   -- matrices in `map_linear_map_add_haar_pi_eq_smul_add_haar`.
@@ -248,33 +248,33 @@ begin
   haveI : is_add_haar_measure (map e μ) := (e : E ≃+ (ι → ℝ)).is_add_haar_measure_map μ Ce Cesymm,
   have ecomp : (e.symm) ∘ e = id,
     by { ext x, simp only [id.def, function.comp_app, linear_equiv.symm_apply_apply] },
-  rw [map_linear_map_add_haar_pi_eq_smul_add_haar hf (map e μ), measure.map_smul,
+  rw [map_linear_map_add_haar_pi_eq_smul_add_haar hf (map e μ), measure.map_smul_nnreal,
     map_map Cesymm.measurable Ce.measurable, ecomp, measure.map_id]
 end
 
 /-- 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
   {f : E →ₗ[ℝ] E} (hf : f.det ≠ 0) (s : set E) :
-  μ (f ⁻¹' s) = ennreal.of_real (abs (f.det)⁻¹) * μ s :=
+  μ (f ⁻¹' s) = ‖(f.det)⁻¹‖₊ • μ s :=
 calc μ (f ⁻¹' s) = measure.map f μ s :
   ((f.equiv_of_det_ne_zero hf).to_continuous_linear_equiv.to_homeomorph
     .to_measurable_equiv.map_apply s).symm
-... = ennreal.of_real (abs (f.det)⁻¹) * μ s :
+... = ‖(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
   {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 :=
+  μ (f ⁻¹' s) = ‖(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
   (f : E ≃ₗ[ℝ] E) (s : set E) :
-  μ (f ⁻¹' s) = ennreal.of_real (abs (f.symm : E →ₗ[ℝ] E).det) * μ s :=
+  μ (f ⁻¹' s) = ‖(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,
@@ -285,14 +285,14 @@ end
 equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
 @[simp] lemma add_haar_preimage_continuous_linear_equiv
   (f : E ≃L[ℝ] E) (s : set E) :
-  μ (f ⁻¹' s) = ennreal.of_real (abs (f.symm : E →ₗ[ℝ] E).det) * μ s :=
+  μ (f ⁻¹' s) = ‖(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
   (f : E →ₗ[ℝ] E) (s : set E) :
-  μ (f '' s) = ennreal.of_real (abs f.det) * μ s :=
+  μ (f '' s) = ‖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,
@@ -302,7 +302,7 @@ begin
     ext x,
     simp only [linear_equiv.coe_to_continuous_linear_equiv, linear_equiv.of_is_unit_det_apply,
                linear_equiv.coe_coe, continuous_linear_equiv.symm_symm], },
-  { simp only [hf, zero_mul, ennreal.of_real_zero, abs_zero],
+  { simp only [hf, zero_smul, ennreal.of_real_zero, nnnorm_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 _) }
@@ -312,22 +312,22 @@ end
 equal to `μ s` times the absolute value of the determinant of `f`. -/
 @[simp] lemma add_haar_image_continuous_linear_map
   (f : E →L[ℝ] E) (s : set E) :
-  μ (f '' s) = ennreal.of_real (abs (f : E →ₗ[ℝ] E).det) * μ s :=
+  μ (f '' s) =‖(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
   (f : E ≃L[ℝ] E) (s : set E) :
-  μ (f '' s) = ennreal.of_real (abs (f : E →ₗ[ℝ] E).det) * μ s :=
+  μ (f '' s) = ‖(f : E →ₗ[ℝ] E).det‖₊ • μ s :=
 μ.add_haar_image_linear_map (f : E →ₗ[ℝ] E) s
 
 /-!
 ### Basic properties of Haar measures on real vector spaces
 -/
 
 lemma map_add_haar_smul {r : ℝ} (hr : r ≠ 0) :
-  measure.map ((•) r) μ = ennreal.of_real (abs (r ^ finrank ℝ E)⁻¹) • μ :=
+  measure.map ((•) r) μ = ‖(r ^ (finrank ℝ E))⁻¹‖₊ • μ :=
 begin
   let f : E →ₗ[ℝ] E := r • 1,
   change measure.map f μ = _,
@@ -340,32 +340,31 @@ begin
 end
 
 @[simp] lemma add_haar_preimage_smul {r : ℝ} (hr : r ≠ 0) (s : set E) :
-  μ (((•) r) ⁻¹' s) = ennreal.of_real (abs (r ^ finrank ℝ E)⁻¹) * μ s :=
+  μ (((•) r) ⁻¹' s) = ‖(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 }
+... = ‖(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)`. -/
 @[simp] lemma add_haar_smul (r : ℝ) (s : set E) :
-  μ (r • s) = ennreal.of_real (abs (r ^ finrank ℝ E)) * μ s :=
+  μ (r • s) = ‖r ^ finrank ℝ E‖₊ • μ s :=
 begin
   rcases ne_or_eq r 0 with h|rfl,
   { rw [← preimage_smul_inv₀ h, add_haar_preimage_smul μ (inv_ne_zero h), inv_pow, inv_inv] },
   rcases eq_empty_or_nonempty s with rfl|hs,
-  { simp only [measure_empty, mul_zero, smul_set_empty] },
+  { simp only [measure_empty, smul_zero, smul_set_empty] },
   rw [zero_smul_set hs, ← singleton_zero],
   by_cases h : finrank ℝ E = 0,
   { haveI : subsingleton E := finrank_zero_iff.1 h,
-    simp only [h, one_mul, ennreal.of_real_one, abs_one, subsingleton.eq_univ_of_nonempty hs,
+    simp only [h, one_smul, nnnorm_one, subsingleton.eq_univ_of_nonempty hs,
       pow_zero, subsingleton.eq_univ_of_nonempty (singleton_nonempty (0 : E))] },
   { haveI : nontrivial E := nontrivial_of_finrank_pos (bot_lt_iff_ne_bot.2 h),
-    simp only [h, zero_mul, ennreal.of_real_zero, abs_zero, ne.def, not_false_iff, zero_pow',
-      measure_singleton] }
+    simp only [h, zero_smul, nnnorm_zero, ne.def, not_false_iff, zero_pow', measure_singleton] }
 end
 
 lemma add_haar_smul_of_nonneg {r : ℝ} (hr : 0 ≤ r) (s : set E) :
-  μ (r • s) = ennreal.of_real (r ^ finrank ℝ E) * μ s :=
-by rw [add_haar_smul, abs_pow, abs_of_nonneg hr]
+  μ (r • s) = (⟨r, hr⟩ ^ finrank ℝ E : ℝ≥0) • μ s :=
+by rw [add_haar_smul, nnnorm_pow, real.nnnorm_of_nonneg]
 
 variables {μ} {s : set E}
 
@@ -381,16 +380,16 @@ begin
   obtain ⟨t, ht, hst⟩ := hs,
   refine ⟨_, ht.const_smul_of_ne_zero hr, _⟩,
   rw ←measure_symm_diff_eq_zero_iff at ⊢ hst,
-  rw [←smul_set_symm_diff₀ hr, add_haar_smul μ, hst, mul_zero],
+  rw [←smul_set_symm_diff₀ hr, add_haar_smul μ, hst, smul_zero],
 end
 
 variables (μ)
 
 @[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 :=
+  μ (affine_map.homothety x r '' s) = ‖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 :
+... = ‖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