Exact source: MathlibAnnex/Analysis/Normed/Sphere/RadialExtension.lean
Pinned GitHub source · Raw UTF-8 source
Back to Isometric unit spheres force equal finite dimensions
1import MathlibAnnex.Analysis.Normed.Sphere.Basic2import Mathlib.Analysis.Normed.Module.Normalize3import Mathlib.Topology.MetricSpace.Isometry4import Mathlib.Topology.MetricSpace.Lipschitz5import Mathlib.Tactic67/-!8# Radial extension of an isometry between unit spheres910Let `e` be a bijective isometry between the unit spheres of two real normed spaces.11This file extends `e` radially by1213`x ↦ ‖x‖ • e (NormedSpace.normalize x)`1415away from the origin, and sends the origin to the origin. The extension preserves16norms, agrees with `e` on the unit sphere, and is a homeomorphism whose forward and17inverse maps are both `3`-Lipschitz.1819The public input type is Mathlib's sphere subtype20`Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1`. The scalar field is21intentionally `ℝ`: no complex-scalar generalization is asserted here. The radial22extension is generally nonlinear and is not asserted to be an isometry of the23ambient spaces. The constant `3` is a certified bound, not an optimality claim.24-/2526noncomputable section2728open Set Metric Function29open scoped NNReal3031namespace MathlibAnnex32namespace Sphere3334universe u v3536variable {X : Type u} {Y : Type v}37 [NormedAddCommGroup X] [NormedSpace ℝ X]38 [NormedAddCommGroup Y] [NormedSpace ℝ Y]3940omit [NormedSpace ℝ X] [NormedSpace ℝ Y] in41@[simp] private theorem sphere_norm_image42 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)43 (u : Metric.sphere (0 : X) 1) :44 ‖(e u : Y)‖ = 1 := norm_eq_of_mem_sphere (e u)4546omit [NormedSpace ℝ X] [NormedSpace ℝ Y] in47private theorem sphere_norm_sub_image48 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)49 (u v : Metric.sphere (0 : X) 1) :50 ‖(e u : Y) - (e v : Y)‖ = ‖(u : X) - (v : X)‖ := by51 have hY : dist (e u : Y) (e v : Y) = dist u v := by52 simpa only [Function.comp_apply] using53 (((isometry_subtype_coe :54 Isometry ((↑) : Metric.sphere (0 : Y) 1 → Y)).comp e.isometry).dist_eq u v)55 have hX : dist (u : X) (v : X) = dist u v :=56 (isometry_subtype_coe :57 Isometry ((↑) : Metric.sphere (0 : X) 1 → X)).dist_eq u v58 calc59 ‖(e u : Y) - (e v : Y)‖ = dist (e u : Y) (e v : Y) :=60 (dist_eq_norm _ _).symm61 _ = dist u v := hY62 _ = dist (u : X) (v : X) := hX.symm63 _ = ‖(u : X) - (v : X)‖ := dist_eq_norm _ _6465omit [NormedSpace ℝ X] in66private theorem abs_norm_sub_le_norm_sub (x y : X) :67 |‖x‖ - ‖y‖| ≤ ‖x - y‖ := by68 refine abs_sub_le_iff.mpr ⟨norm_sub_norm_le x y, ?_⟩69 simpa only [norm_sub_rev] using (norm_sub_norm_le y x)7071/-- The angular part of the radial estimate. The smaller radius multiplies the72change of normalized directions, producing a bound by twice the ambient chord. -/73theorem scaled_normalize_dist_le_two74 {x y : X} (hx : x ≠ 0) (hy : y ≠ 0) (hyx : ‖y‖ ≤ ‖x‖) :75 ‖y‖ * ‖NormedSpace.normalize x - NormedSpace.normalize y‖ ≤76 2 * ‖x - y‖ := by77 let q : ℝ := ‖y‖ / ‖x‖78 have hnx : 0 < ‖x‖ := norm_pos_iff.mpr hx79 have hny : 0 ≤ ‖y‖ := norm_nonneg y80 have hq0 : 0 ≤ q := div_nonneg hny hnx.le81 have hq1 : q ≤ 1 := (div_le_one hnx).2 hyx82 have hqnx : q * ‖x‖ = ‖y‖ := by83 dsimp [q]84 field_simp [ne_of_gt hnx]85 have hscaled :86 ‖y‖ • (NormedSpace.normalize x - NormedSpace.normalize y) =87 q • x - y := by88 simp [NormedSpace.normalize, q, smul_sub, smul_smul, div_eq_mul_inv,89 norm_ne_zero_iff.mpr hy]90 have hdecomp :91 q • x - y = q • (x - y) + (q - 1) • y := by92 module93 have hfirst : ‖q • (x - y)‖ ≤ ‖x - y‖ := by94 rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg hq0]95 nlinarith [norm_nonneg (x - y)]96 have habs : |q - 1| = 1 - q := by97 rw [abs_of_nonpos (sub_nonpos.mpr hq1)]98 ring99 have hsecond : ‖(q - 1) • y‖ ≤ ‖x - y‖ := by100 rw [norm_smul, Real.norm_eq_abs, habs]101 have hfactor : 0 ≤ 1 - q := sub_nonneg.mpr hq1102 calc103 (1 - q) * ‖y‖ ≤ (1 - q) * ‖x‖ :=104 mul_le_mul_of_nonneg_left hyx hfactor105 _ = ‖x‖ - ‖y‖ := by nlinarith [hqnx]106 _ = |‖x‖ - ‖y‖| := by rw [abs_of_nonneg (sub_nonneg.mpr hyx)]107 _ ≤ ‖x - y‖ := abs_norm_sub_le_norm_sub x y108 calc109 ‖y‖ * ‖NormedSpace.normalize x - NormedSpace.normalize y‖ =110 ‖‖y‖ • (NormedSpace.normalize x - NormedSpace.normalize y)‖ := by111 rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg hny]112 _ = ‖q • x - y‖ := by rw [hscaled]113 _ = ‖q • (x - y) + (q - 1) • y‖ := by rw [hdecomp]114 _ ≤ ‖q • (x - y)‖ + ‖(q - 1) • y‖ := norm_add_le _ _115 _ ≤ ‖x - y‖ + ‖x - y‖ := add_le_add hfirst hsecond116 _ = 2 * ‖x - y‖ := by ring117118/-- Homogeneous radial extension of an isometry equivalence between unit spheres.119The origin is treated separately. -/120def radialExtension121 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) (x : X) : Y := by122 classical123 exact if hx : x = 0 then 0 else124 ‖x‖ • (e (normalizeToSphere x hx) : Y)125126@[simp] theorem radialExtension_zero127 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :128 radialExtension e 0 = 0 := by129 simp [radialExtension]130131theorem radialExtension_of_ne_zero132 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)133 {x : X} (hx : x ≠ 0) :134 radialExtension e x = ‖x‖ • (e (normalizeToSphere x hx) : Y) := by135 simp [radialExtension, hx]136137/-- The radial extension preserves the norm of every vector. -/138@[simp] theorem radialExtension_norm139 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) (x : X) :140 ‖radialExtension e x‖ = ‖x‖ := by141 by_cases hx : x = 0142 · simp [hx]143 · rw [radialExtension_of_ne_zero e hx, norm_smul]144 simp145146/-- On the unit sphere, the radial extension agrees with the original map. -/147@[simp] theorem radialExtension_on_sphere148 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)149 (u : Metric.sphere (0 : X) 1) :150 radialExtension e (u : X) = (e u : Y) := by151 rw [radialExtension_of_ne_zero e (ne_zero_of_mem_unit_sphere u)]152 simp153154/-- Radial extensions of inverse sphere isometries are left inverses. -/155theorem radialExtension_leftInverse156 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :157 LeftInverse (radialExtension e.symm) (radialExtension e) := by158 intro x159 by_cases hx : x = 0160 · simp [hx]161 · have hHx : radialExtension e x ≠ 0 := by162 intro hzero163 have : ‖x‖ = 0 := by simpa using congrArg norm hzero164 exact hx (norm_eq_zero.mp this)165 rw [radialExtension_of_ne_zero e.symm hHx]166 have hnorm : ‖radialExtension e x‖ = ‖x‖ := radialExtension_norm e x167 rw [hnorm]168 have hdir :169 normalizeToSphere (radialExtension e x) hHx =170 e (normalizeToSphere x hx) := by171 apply Subtype.ext172 change NormedSpace.normalize (radialExtension e x) =173 (e (normalizeToSphere x hx) : Y)174 rw [radialExtension_of_ne_zero e hx]175 rw [NormedSpace.normalize_smul_of_pos (norm_pos_iff.mpr hx)]176 exact NormedSpace.normalize_eq_self_of_norm_eq_one177 (sphere_norm_image e (normalizeToSphere x hx))178 rw [hdir, e.symm_apply_apply]179 exact NormedSpace.norm_smul_normalize x180181/-- The opposite composition is proved separately by applying the left-inverse182result to the inverse sphere isometry. -/183theorem radialExtension_rightInverse184 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :185 RightInverse (radialExtension e.symm) (radialExtension e) := by186 exact radialExtension_leftInverse e.symm187188private theorem radialExtension_dist_le_three_of_norm_le189 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)190 {x y : X} (hyx : ‖y‖ ≤ ‖x‖) :191 ‖radialExtension e x - radialExtension e y‖ ≤ 3 * ‖x - y‖ := by192 by_cases hy : y = 0193 · subst y194 simp [radialExtension_norm]195 nlinarith [norm_nonneg x]196 have hx : x ≠ 0 := by197 intro hx0198 subst x199 have hy0 : ‖y‖ = 0 := le_antisymm (by simpa using hyx) (norm_nonneg y)200 exact hy (norm_eq_zero.mp hy0)201 let ux : Metric.sphere (0 : X) 1 := normalizeToSphere x hx202 let uy : Metric.sphere (0 : X) 1 := normalizeToSphere y hy203 let ax : Y := (e ux : Y)204 let ay : Y := (e uy : Y)205 have hsplit :206 ‖x‖ • ax - ‖y‖ • ay =207 (‖x‖ • ax - ‖y‖ • ax) + (‖y‖ • ax - ‖y‖ • ay) := by208 module209 have hcoeff : ‖‖x‖ • ax - ‖y‖ • ax‖ = |‖x‖ - ‖y‖| := by210 rw [← sub_smul, norm_smul]211 simp [ax, Real.norm_eq_abs]212 have hang :213 ‖‖y‖ • ax - ‖y‖ • ay‖ =214 ‖y‖ * ‖NormedSpace.normalize x - NormedSpace.normalize y‖ := by215 rw [← smul_sub, norm_smul, Real.norm_eq_abs,216 abs_of_nonneg (norm_nonneg y)]217 congr 1218 exact sphere_norm_sub_image e ux uy219 rw [radialExtension_of_ne_zero e hx, radialExtension_of_ne_zero e hy]220 change ‖‖x‖ • ax - ‖y‖ • ay‖ ≤ 3 * ‖x - y‖221 rw [hsplit]222 calc223 ‖(‖x‖ • ax - ‖y‖ • ax) + (‖y‖ • ax - ‖y‖ • ay)‖224 ≤ ‖‖x‖ • ax - ‖y‖ • ax‖ + ‖‖y‖ • ax - ‖y‖ • ay‖ :=225 norm_add_le _ _226 _ = |‖x‖ - ‖y‖| +227 ‖y‖ * ‖NormedSpace.normalize x - NormedSpace.normalize y‖ := by228 rw [hcoeff, hang]229 _ ≤ ‖x - y‖ + 2 * ‖x - y‖ :=230 add_le_add (abs_norm_sub_le_norm_sub x y)231 (scaled_normalize_dist_le_two hx hy hyx)232 _ = 3 * ‖x - y‖ := by ring233234private theorem radialExtension_dist_le_three235 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) (x y : X) :236 ‖radialExtension e x - radialExtension e y‖ ≤ 3 * ‖x - y‖ := by237 rcases le_total ‖y‖ ‖x‖ with hyx | hxy238 · exact radialExtension_dist_le_three_of_norm_le e hyx239 · have h := radialExtension_dist_le_three_of_norm_le e (x := y) (y := x) hxy240 simpa [norm_sub_rev] using h241242/-- The forward radial extension is globally `3`-Lipschitz. -/243theorem lipschitzWith_radialExtension244 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :245 LipschitzWith 3 (radialExtension e) := by246 refine LipschitzWith.of_dist_le_mul ?_247 intro x y248 simpa [dist_eq_norm] using radialExtension_dist_le_three e x y249250/-- The radial extension associated with the inverse sphere isometry is also251`3`-Lipschitz. -/252theorem lipschitzWith_radialExtension_symm253 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :254 LipschitzWith 3 (radialExtension e.symm) :=255 lipschitzWith_radialExtension e.symm256257/-- The radial extension and the extension of the inverse sphere isometry form258an equivalence of the ambient spaces. -/259noncomputable def radialExtensionEquiv260 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) : X ≃ Y where261 toFun := radialExtension e262 invFun := radialExtension e.symm263 left_inv := radialExtension_leftInverse e264 right_inv := radialExtension_rightInverse e265266theorem radialExtension_surjective267 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :268 Surjective (radialExtension e) :=269 (radialExtension_rightInverse e).surjective270271/-- Norm-preserving homeomorphism obtained from the radial extension. This is272not asserted to be linear or an ambient isometry. -/273noncomputable def radialExtensionHomeomorph274 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) : X ≃ₜ Y where275 toEquiv := radialExtensionEquiv e276 continuous_toFun := (lipschitzWith_radialExtension e).continuous277 continuous_invFun := (lipschitzWith_radialExtension_symm e).continuous278279end Sphere280end MathlibAnnex