feat(Analysis.NormedSpace): add normalized vectors (#26308)

Add normalized vectors to Mathlib (zero vector for zero vector, the corresponding unit vectors for nonzero vectors)

Author: LessnessRandomness

Mathlib.lean

@@ -1863,6 +1863,7 @@ import Mathlib.Analysis.NormedSpace.MStructure
 import Mathlib.Analysis.NormedSpace.Multilinear.Basic
 import Mathlib.Analysis.NormedSpace.Multilinear.Curry
 import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
+import Mathlib.Analysis.NormedSpace.Normalize
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear

Mathlib/Analysis/NormedSpace/Normalize.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2025 Ilmārs Cīrulis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ilmārs Cīrulis, Alex Meiburg
+-/
+import Mathlib.Analysis.RCLike.Basic
+
+/-!
+# Normalized vector
+
+Function that returns unit length vector that points in the same direction
+(if the given vector is nonzero vector) or returns zero vector
+(if the given vector is zero vector).
+-/
+
+variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
+
+/-- For a nonzero vector `x`, `normalize x` is the unit-length vector that points
+in the same direction as `x`. If `x = 0`, then `normalize x = 0`. -/
+noncomputable def NormedSpace.normalize (x : V) : V := ‖x‖⁻¹ • x
+
+namespace NormedSpace
+
+@[simp]
+theorem normalize_zero_eq_zero : normalize (0 : V) = 0 := by
+  simp [normalize]
+
+@[simp]
+theorem norm_smul_normalize (x : V) : ‖x‖ • normalize x = x := by
+  by_cases hx : x = 0
+  all_goals simp [normalize, hx]
+
+@[simp]
+lemma norm_normalize_eq_one_iff {x : V} : ‖normalize x‖ = 1 ↔ x ≠ 0 :=
+  ⟨by rintro hx rfl; simp at hx, fun h ↦ by simp [normalize, h, norm_smul]⟩
+
+lemma normalize_eq_self_of_norm_eq_one {x : V} (h : ‖x‖ = 1) : normalize x = x := by
+  simp [normalize, h]
+
+@[simp]
+theorem normalize_normalize (x : V) : normalize (normalize x) = normalize x := by
+  by_cases hx : x = 0
+  · simp [hx]
+  · simp [normalize_eq_self_of_norm_eq_one, hx]
+
+@[simp]
+theorem normalize_neg (x : V) : normalize (- x) = - normalize x := by
+  simp [normalize]
+
+theorem normalize_smul_of_pos {r : ℝ} (hr : 0 < r) (x : V) :
+    normalize (r • x) = normalize x := by
+  simp [normalize, norm_smul, smul_smul, abs_of_pos hr, mul_assoc, inv_mul_cancel₀ hr.ne']
+
+theorem normalize_smul_of_neg {r : ℝ} (hr : r < 0) (x : V) :
+    normalize (r • x) = - normalize x := by
+  simpa using normalize_smul_of_pos (show 0 < -r by linarith) (-x)
+
+end NormedSpace