feat(data/real/nnreal): upgrade nnabs to a monoid_with_zero_hom (#…

…8844)

Other changes:

* add `nnreal.finset_sup_div`;
* rename `nnreal.coe_nnabs` to `real.coe_nnabs`;
* add `real.nndist_eq` and `real.nndist_eq'`.

src/analysis/calculus/parametric_integral.lean

@@ -82,7 +82,7 @@ begin
       intros a ha,
       rw lipschitz_on_with_iff_norm_sub_le at ha,
       apply (ha x₀ x₀_in x x_in).trans,
-      rw [mul_comm, nnreal.coe_nnabs, real.norm_eq_abs],
+      rw [mul_comm, real.coe_nnabs, real.norm_eq_abs],
       rw [mem_ball, dist_eq_norm, norm_sub_rev] at x_in,
       exact mul_le_mul_of_nonneg_right (le_of_lt x_in) (abs_nonneg  _) },
     exact integrable_of_norm_sub_le (hF_meas x x_in) hF_int
@@ -198,7 +198,7 @@ begin
     rintros a ⟨ha_deriv, ha_bound⟩,
     refine (convex_ball _ _).lipschitz_on_with_of_nnnorm_has_fderiv_within_le
       (λ x x_in, (ha_deriv x x_in).has_fderiv_within_at) (λ x x_in, _),
-    rw [← nnreal.coe_le_coe, coe_nnnorm, nnreal.coe_nnabs],
+    rw [← nnreal.coe_le_coe, coe_nnnorm, real.coe_nnabs],
     exact (ha_bound x x_in).trans (le_abs_self _) },
   exact (has_fderiv_at_of_dominated_loc_of_lip ε_pos hF_meas hF_int
                                                hF'_meas this bound_integrable diff_x₀).2
@@ -255,7 +255,7 @@ begin
     rintros a ⟨ha_deriv, ha_bound⟩,
     refine (convex_ball _ _).lipschitz_on_with_of_nnnorm_has_deriv_within_le
       (λ x x_in, (ha_deriv x x_in).has_deriv_within_at) (λ x x_in, _),
-    rw [← nnreal.coe_le_coe, coe_nnnorm, nnreal.coe_nnabs],
+    rw [← nnreal.coe_le_coe, coe_nnnorm, real.coe_nnabs],
     exact (ha_bound x x_in).trans (le_abs_self _) },
   exact has_deriv_at_of_dominated_loc_of_lip ε_pos hF_meas hF_int hF'_meas this
         bound_integrable diff_x₀

src/data/real/nnreal.lean

@@ -393,6 +393,10 @@ begin
   { assume a s has ih, simp [has, ih, mul_sup], }
 end
 
+lemma finset_sup_div {α} {f : α → ℝ≥0} {s : finset α} (r : ℝ≥0) :
+  s.sup f / r = s.sup (λ a, f a / r) :=
+by simp only [div_eq_inv_mul, mul_finset_sup]
+
 @[simp, norm_cast] lemma coe_max (x y : ℝ≥0) :
   ((max x y : ℝ≥0) : ℝ) = max (x : ℝ) (y : ℝ) :=
 by { delta max, split_ifs; refl }
@@ -763,19 +767,26 @@ abs_of_nonneg x.property
 
 end nnreal
 
+namespace real
+
 /-- The absolute value on `ℝ` as a map to `ℝ≥0`. -/
-@[pp_nodot] def real.nnabs (x : ℝ) : ℝ≥0 := ⟨abs x, abs_nonneg x⟩
+@[pp_nodot] def nnabs : monoid_with_zero_hom ℝ ℝ≥0 :=
+{ to_fun := λ x, ⟨abs x, abs_nonneg x⟩,
+  map_zero' := by { ext, simp },
+  map_one' := by { ext, simp },
+  map_mul' := λ x y, by { ext, simp [abs_mul] } }
 
-@[norm_cast, simp] lemma nnreal.coe_nnabs (x : ℝ) : (real.nnabs x : ℝ) = abs x :=
-by simp [real.nnabs]
+@[norm_cast, simp] lemma coe_nnabs (x : ℝ) : (nnabs x : ℝ) = abs x :=
+by simp [nnabs]
 
-@[simp]
-lemma real.nnabs_of_nonneg {x : ℝ} (h : 0 ≤ x) : real.nnabs x = real.to_nnreal x :=
-by { ext, simp [real.coe_to_nnreal x h, abs_of_nonneg h] }
+@[simp] lemma nnabs_of_nonneg {x : ℝ} (h : 0 ≤ x) : nnabs x = to_nnreal x :=
+by { ext, simp [coe_to_nnreal x h, abs_of_nonneg h] }
 
-lemma real.coe_to_nnreal_le (x : ℝ) : (real.to_nnreal x : ℝ) ≤ abs x :=
+lemma coe_to_nnreal_le (x : ℝ) : (to_nnreal x : ℝ) ≤ abs x :=
 max_le (le_abs_self _) (abs_nonneg _)
 
 lemma cast_nat_abs_eq_nnabs_cast (n : ℤ) :
-  (n.nat_abs : ℝ≥0) = real.nnabs n :=
-by { ext, rw [nnreal.coe_nat_cast, int.cast_nat_abs, nnreal.coe_nnabs] }
+  (n.nat_abs : ℝ≥0) = nnabs n :=
+by { ext, rw [nnreal.coe_nat_cast, int.cast_nat_abs, real.coe_nnabs] }
+
+end real

src/topology/metric_space/basic.lean

@@ -928,6 +928,10 @@ instance real.pseudo_metric_space : pseudo_metric_space ℝ :=
 
 theorem real.dist_eq (x y : ℝ) : dist x y = abs (x - y) := rfl
 
+theorem real.nndist_eq (x y : ℝ) : nndist x y = real.nnabs (x - y) := rfl
+
+theorem real.nndist_eq' (x y : ℝ) : nndist x y = real.nnabs (y - x) := nndist_comm _ _
+
 theorem real.dist_0_eq_abs (x : ℝ) : dist x 0 = abs x :=
 by simp [real.dist_eq]