chore(analysis/normed/group/add_torsor): nnnorm lemmas (#18997)

For every `dist`/`norm` lemma in these files, this adds the corresponding `nndist`/`nnnorm` lemma.

src/analysis/normed/group/add_torsor.lean

@@ -68,12 +68,18 @@ lemma, it is necessary to have `V` as an explicit argument; otherwise
 `rw dist_eq_norm_vsub` sometimes doesn't work. -/
 lemma dist_eq_norm_vsub (x y : P) : dist x y = ‖x -ᵥ y‖ := normed_add_torsor.dist_eq_norm' x y
 
+lemma nndist_eq_nnnorm_vsub (x y : P) : nndist x y = ‖x -ᵥ y‖₊ :=
+nnreal.eq $ dist_eq_norm_vsub V x y
+
 /-- The distance equals the norm of subtracting two points. In this
 lemma, it is necessary to have `V` as an explicit argument; otherwise
 `rw dist_eq_norm_vsub'` sometimes doesn't work. -/
 lemma dist_eq_norm_vsub' (x y : P) : dist x y = ‖y -ᵥ x‖ :=
 (dist_comm _ _).trans (dist_eq_norm_vsub _ _ _)
 
+lemma nndist_eq_nnnorm_vsub' (x y : P) : nndist x y = ‖y -ᵥ x‖₊ :=
+nnreal.eq $ dist_eq_norm_vsub' V x y
+
 end
 
 lemma dist_vadd_cancel_left (v : V) (x y : P) :
@@ -84,12 +90,22 @@ dist_vadd _ _ _
   dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂ :=
 by rw [dist_eq_norm_vsub V, dist_eq_norm, vadd_vsub_vadd_cancel_right]
 
+@[simp] lemma nndist_vadd_cancel_right (v₁ v₂ : V) (x : P) :
+  nndist (v₁ +ᵥ x) (v₂ +ᵥ x) = nndist v₁ v₂ :=
+nnreal.eq $ dist_vadd_cancel_right _ _ _
+
 @[simp] lemma dist_vadd_left (v : V) (x : P) : dist (v +ᵥ x) x = ‖v‖ :=
 by simp [dist_eq_norm_vsub V _ x]
 
+@[simp] lemma nndist_vadd_left (v : V) (x : P) : nndist (v +ᵥ x) x = ‖v‖₊ :=
+nnreal.eq $ dist_vadd_left _ _
+
 @[simp] lemma dist_vadd_right (v : V) (x : P) : dist x (v +ᵥ x) = ‖v‖ :=
 by rw [dist_comm, dist_vadd_left]
 
+@[simp] lemma nndist_vadd_right (v : V) (x : P) : nndist x (v +ᵥ x) = ‖v‖₊ :=
+nnreal.eq $ dist_vadd_right _ _
+
 /-- Isometry between the tangent space `V` of a (semi)normed add torsor `P` and `P` given by
 addition/subtraction of `x : P`. -/
 @[simps] def isometry_equiv.vadd_const (x : P) : V ≃ᵢ P :=
@@ -108,19 +124,22 @@ subtraction from `x : P`. -/
 @[simp] lemma dist_vsub_cancel_right (x y z : P) : dist (x -ᵥ z) (y -ᵥ z) = dist x y :=
 (isometry_equiv.vadd_const z).symm.dist_eq x y
 
+@[simp] lemma nndist_vsub_cancel_right (x y z : P) : nndist (x -ᵥ z) (y -ᵥ z) = nndist x y :=
+nnreal.eq $ dist_vsub_cancel_right _ _ _
+
 lemma dist_vadd_vadd_le (v v' : V) (p p' : P) :
   dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p' :=
 by simpa using dist_triangle (v +ᵥ p) (v' +ᵥ p) (v' +ᵥ p')
 
+lemma nndist_vadd_vadd_le (v v' : V) (p p' : P) :
+  nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p' :=
+dist_vadd_vadd_le _ _ _ _
+
 lemma dist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
   dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄ :=
 by { rw [dist_eq_norm, vsub_sub_vsub_comm, dist_eq_norm_vsub V, dist_eq_norm_vsub V],
  exact norm_sub_le _ _ }
 
-lemma nndist_vadd_vadd_le (v v' : V) (p p' : P) :
-  nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p' :=
-by simp only [← nnreal.coe_le_coe, nnreal.coe_add, ← dist_nndist, dist_vadd_vadd_le]
-
 lemma nndist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
   nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄ :=
 by simp only [← nnreal.coe_le_coe, nnreal.coe_add, ← dist_nndist, dist_vsub_vsub_le]

src/analysis/normed_space/add_torsor.lean

@@ -46,10 +46,18 @@ include V
   dist p₁ (homothety p₁ c p₂) = ‖c‖ * dist p₁ p₂ :=
 by simp [homothety_def, norm_smul, ← dist_eq_norm_vsub, dist_comm]
 
+@[simp] lemma nndist_center_homothety (p₁ p₂ : P) (c : 𝕜) :
+  nndist p₁ (homothety p₁ c p₂) = ‖c‖₊ * nndist p₁ p₂ :=
+nnreal.eq $ dist_center_homothety _ _ _
+
 @[simp] lemma dist_homothety_center (p₁ p₂ : P) (c : 𝕜) :
   dist (homothety p₁ c p₂) p₁ = ‖c‖ * dist p₁ p₂ :=
 by rw [dist_comm, dist_center_homothety]
 
+@[simp] lemma nndist_homothety_center (p₁ p₂ : P) (c : 𝕜) :
+  nndist (homothety p₁ c p₂) p₁ = ‖c‖₊ * nndist p₁ p₂ :=
+nnreal.eq $ dist_homothety_center _ _ _
+
 @[simp] lemma dist_line_map_line_map (p₁ p₂ : P) (c₁ c₂ : 𝕜) :
   dist (line_map p₁ p₂ c₁) (line_map p₁ p₂ c₂) = dist c₁ c₂ * dist p₁ p₂ :=
 begin
@@ -58,6 +66,10 @@ begin
     vsub_eq_sub],
 end
 
+@[simp] lemma nndist_line_map_line_map (p₁ p₂ : P) (c₁ c₂ : 𝕜) :
+  nndist (line_map p₁ p₂ c₁) (line_map p₁ p₂ c₂) = nndist c₁ c₂ * nndist p₁ p₂ :=
+nnreal.eq $ dist_line_map_line_map _ _ _ _
+
 lemma lipschitz_with_line_map (p₁ p₂ : P) :
   lipschitz_with (nndist p₁ p₂) (line_map p₁ p₂ : 𝕜 → P) :=
 lipschitz_with.of_dist_le_mul $ λ c₁ c₂,
@@ -67,26 +79,50 @@ lipschitz_with.of_dist_le_mul $ λ c₁ c₂,
   dist (line_map p₁ p₂ c) p₁ = ‖c‖ * dist p₁ p₂ :=
 by simpa only [line_map_apply_zero, dist_zero_right] using dist_line_map_line_map p₁ p₂ c 0
 
+@[simp] lemma nndist_line_map_left (p₁ p₂ : P) (c : 𝕜) :
+  nndist (line_map p₁ p₂ c) p₁ = ‖c‖₊ * nndist p₁ p₂ :=
+nnreal.eq $ dist_line_map_left _ _ _
+
 @[simp] lemma dist_left_line_map (p₁ p₂ : P) (c : 𝕜) :
   dist p₁ (line_map p₁ p₂ c) = ‖c‖ * dist p₁ p₂ :=
 (dist_comm _ _).trans (dist_line_map_left _ _ _)
 
+@[simp] lemma nndist_left_line_map (p₁ p₂ : P) (c : 𝕜) :
+  nndist p₁ (line_map p₁ p₂ c) = ‖c‖₊ * nndist p₁ p₂ :=
+nnreal.eq $ dist_left_line_map _ _ _
+
 @[simp] lemma dist_line_map_right (p₁ p₂ : P) (c : 𝕜) :
   dist (line_map p₁ p₂ c) p₂ = ‖1 - c‖ * dist p₁ p₂ :=
 by simpa only [line_map_apply_one, dist_eq_norm'] using dist_line_map_line_map p₁ p₂ c 1
 
+@[simp] lemma nndist_line_map_right (p₁ p₂ : P) (c : 𝕜) :
+  nndist (line_map p₁ p₂ c) p₂ = ‖1 - c‖₊ * nndist p₁ p₂ :=
+nnreal.eq $ dist_line_map_right _ _ _
+
 @[simp] lemma dist_right_line_map (p₁ p₂ : P) (c : 𝕜) :
   dist p₂ (line_map p₁ p₂ c) = ‖1 - c‖ * dist p₁ p₂ :=
 (dist_comm _ _).trans (dist_line_map_right _ _ _)
 
+@[simp] lemma nndist_right_line_map (p₁ p₂ : P) (c : 𝕜) :
+  nndist p₂ (line_map p₁ p₂ c) = ‖1 - c‖₊ * nndist p₁ p₂ :=
+nnreal.eq $ dist_right_line_map _ _ _
+
 @[simp] lemma dist_homothety_self (p₁ p₂ : P) (c : 𝕜) :
   dist (homothety p₁ c p₂) p₂ = ‖1 - c‖ * dist p₁ p₂ :=
 by rw [homothety_eq_line_map, dist_line_map_right]
 
+@[simp] lemma nndist_homothety_self (p₁ p₂ : P) (c : 𝕜) :
+  nndist (homothety p₁ c p₂) p₂ = ‖1 - c‖₊ * nndist p₁ p₂ :=
+nnreal.eq $ dist_homothety_self _ _ _
+
 @[simp] lemma dist_self_homothety (p₁ p₂ : P) (c : 𝕜) :
   dist p₂ (homothety p₁ c p₂) = ‖1 - c‖ * dist p₁ p₂ :=
 by rw [dist_comm, dist_homothety_self]
 
+@[simp] lemma nndist_self_homothety (p₁ p₂ : P) (c : 𝕜) :
+  nndist p₂ (homothety p₁ c p₂) = ‖1 - c‖₊ * nndist p₁ p₂ :=
+nnreal.eq $ dist_self_homothety _ _ _
+
 section invertible_two
 
 variables [invertible (2:𝕜)]
@@ -95,18 +131,34 @@ variables [invertible (2:𝕜)]
   dist p₁ (midpoint 𝕜 p₁ p₂) = ‖(2:𝕜)‖⁻¹ * dist p₁ p₂ :=
 by rw [midpoint, dist_comm, dist_line_map_left, inv_of_eq_inv, ← norm_inv]
 
+@[simp] lemma nndist_left_midpoint (p₁ p₂ : P) :
+  nndist p₁ (midpoint 𝕜 p₁ p₂) = ‖(2:𝕜)‖₊⁻¹ * nndist p₁ p₂ :=
+nnreal.eq $ dist_left_midpoint _ _
+
 @[simp] lemma dist_midpoint_left (p₁ p₂ : P) :
   dist (midpoint 𝕜 p₁ p₂) p₁ = ‖(2:𝕜)‖⁻¹ * dist p₁ p₂ :=
 by rw [dist_comm, dist_left_midpoint]
 
+@[simp] lemma nndist_midpoint_left (p₁ p₂ : P) :
+  nndist (midpoint 𝕜 p₁ p₂) p₁ = ‖(2:𝕜)‖₊⁻¹ * nndist p₁ p₂ :=
+nnreal.eq $ dist_midpoint_left _ _
+
 @[simp] lemma dist_midpoint_right (p₁ p₂ : P) :
   dist (midpoint 𝕜 p₁ p₂) p₂ = ‖(2:𝕜)‖⁻¹ * dist p₁ p₂ :=
 by rw [midpoint_comm, dist_midpoint_left, dist_comm]
 
+@[simp] lemma nndist_midpoint_right (p₁ p₂ : P) :
+  nndist (midpoint 𝕜 p₁ p₂) p₂ = ‖(2:𝕜)‖₊⁻¹ * nndist p₁ p₂ :=
+nnreal.eq $ dist_midpoint_right _ _
+
 @[simp] lemma dist_right_midpoint (p₁ p₂ : P) :
   dist p₂ (midpoint 𝕜 p₁ p₂) = ‖(2:𝕜)‖⁻¹ * dist p₁ p₂ :=
 by rw [dist_comm, dist_midpoint_right]
 
+@[simp] lemma nndist_right_midpoint (p₁ p₂ : P) :
+  nndist p₂ (midpoint 𝕜 p₁ p₂) = ‖(2:𝕜)‖₊⁻¹ * nndist p₁ p₂ :=
+nnreal.eq $ dist_right_midpoint _ _
+
 lemma dist_midpoint_midpoint_le' (p₁ p₂ p₃ p₄ : P) :
   dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖(2 : 𝕜)‖ :=
 begin
@@ -116,6 +168,10 @@ begin
   exact div_le_div_of_le_of_nonneg (norm_add_le _ _) (norm_nonneg _),
 end
 
+lemma nndist_midpoint_midpoint_le' (p₁ p₂ p₃ p₄ : P) :
+  nndist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (nndist p₁ p₃ + nndist p₂ p₄) / ‖(2 : 𝕜)‖₊ :=
+dist_midpoint_midpoint_le' _ _ _ _
+
 end invertible_two
 
 omit V
@@ -160,6 +216,10 @@ lemma dist_midpoint_midpoint_le (p₁ p₂ p₃ p₄ : V) :
   dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2 :=
 by simpa using dist_midpoint_midpoint_le' p₁ p₂ p₃ p₄
 
+lemma nndist_midpoint_midpoint_le (p₁ p₂ p₃ p₄ : V) :
+  nndist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (nndist p₁ p₃ + nndist p₂ p₄) / 2 :=
+dist_midpoint_midpoint_le _ _ _ _
+
 include V W
 
 /-- A continuous map between two normed affine spaces is an affine map provided that