Exact source: MathlibAnnex/Analysis/Normed/Sphere/Basic.lean
Pinned GitHub source · Raw UTF-8 source
Back to Radial extension of an isometry between unit spheres
1import Mathlib.Analysis.Normed.Module.Normalize2import Mathlib.Topology.MetricSpace.Isometry34/-!5# Normalization into the unit sphere67Package ambient normalization as a sphere element, with its retraction and8positive radial scaling laws. No nontriviality assumption is required.9-/1011namespace MathlibAnnex.Sphere1213variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]1415/-- The unit direction of a nonzero vector. -/16noncomputable def normalizeToSphere (x : E) (hx : x ≠ 0) :17 Metric.sphere (0 : E) 1 :=18 ⟨NormedSpace.normalize x, by19 simpa [dist_eq_norm] using NormedSpace.norm_normalize hx⟩2021@[simp] theorem coe_normalizeToSphere (x : E) (hx : x ≠ 0) :22 (normalizeToSphere x hx : E) = NormedSpace.normalize x := rfl2324/-- Normalization retracts the unit sphere. -/25@[simp] theorem normalizeToSphere_unit (u : Metric.sphere (0 : E) 1) :26 normalizeToSphere (u : E) (ne_zero_of_mem_unit_sphere u) = u := by27 apply Subtype.ext28 exact NormedSpace.normalize_eq_self_of_norm_eq_one (norm_eq_of_mem_sphere u)2930/-- A positive change of radius preserves the unit direction. -/31theorem normalizeToSphere_pos_smul (u : Metric.sphere (0 : E) 1)32 {r : ℝ} (hr : 0 < r) :33 normalizeToSphere (r • (u : E))34 (smul_ne_zero hr.ne' (ne_zero_of_mem_unit_sphere u)) = u := by35 apply Subtype.ext36 change NormedSpace.normalize (r • (u : E)) = (u : E)37 rw [NormedSpace.normalize_smul_of_pos hr]38 exact NormedSpace.normalize_eq_self_of_norm_eq_one (norm_eq_of_mem_sphere u)3940end MathlibAnnex.Sphere