From 837f72de63ad6cd96519cde5f1ffd5ed8d280ad0 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 29 May 2023 17:56:41 +0000 Subject: [PATCH] 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 | 27 ++++++++-- src/analysis/normed_space/add_torsor.lean | 60 +++++++++++++++++++++++ 2 files changed, 83 insertions(+), 4 deletions(-) diff --git a/src/analysis/normed/group/add_torsor.lean b/src/analysis/normed/group/add_torsor.lean index 169615af036ed..6642720beafb0 100644 --- a/src/analysis/normed/group/add_torsor.lean +++ b/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] diff --git a/src/analysis/normed_space/add_torsor.lean b/src/analysis/normed_space/add_torsor.lean index 001c01845a245..21887171303ef 100644 --- a/src/analysis/normed_space/add_torsor.lean +++ b/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