Exact UTF-8 source: MathlibAnnex/Analysis/Normed/Affine/IsometryExtension/Local.lean
Download exact raw UTF-8 source
1import MathlibAnnex.Analysis.Normed.Affine.Reflection2import Mathlib.Analysis.Convex.Basic3import Mathlib.Analysis.Normed.Affine.AddTorsor4import Mathlib.Analysis.Normed.Module.Convex5import Mathlib.LinearAlgebra.AffineSpace.MidpointZero6import Mathlib.Tactic.Linarith7import Mathlib.Tactic.Module8import Mathlib.Tactic.NormNum9import Mathlib.Tactic.Order10import Mathlib.Tactic.Positivity11import Mathlib.Tactic.Ring1213/-!14# Local extension machinery for isometries1516This module develops the local midpoint and affine-segment identities used to17extend isometries between open subsets of real normed spaces.18-/1920open Metric Set AffineIsometryEquiv Bornology2122namespace MathlibAnnex2324noncomputable section2526variable {E F : Type*}27 [NormedAddCommGroup E] [NormedSpace ℝ E]28 [NormedAddCommGroup F] [NormedSpace ℝ F]2930/-- The intersection of two closed balls with the same radius. -/31def symmetricLens (x y : E) (r : ℝ) : Set E :=32 closedBall x r ∩ closedBall y r3334private theorem midpoint_mem_symmetricLens {x y : E} {r : ℝ}35 (h : 2⁻¹ * dist x y ≤ r) : midpoint ℝ x y ∈ symmetricLens x y r := by36 constructor37 · simpa [symmetricLens, dist_midpoint_left, Real.norm_two] using h38 · simpa [symmetricLens, dist_midpoint_right, Real.norm_two] using h3940private theorem symmetricLens_reflectionInvariant (x y : E) (r : ℝ) :41 MapsTo (pointReflection ℝ (midpoint ℝ x y))42 (symmetricLens x y r) (symmetricLens x y r) := by43 rintro z ⟨hzx, hzy⟩44 constructor45 · change dist (pointReflection ℝ (midpoint ℝ x y) z) x ≤ r46 calc47 dist (pointReflection ℝ (midpoint ℝ x y) z) x =48 dist (pointReflection ℝ (midpoint ℝ x y) z)49 (pointReflection ℝ (midpoint ℝ x y) y) :=50 congrArg (dist (pointReflection ℝ (midpoint ℝ x y) z))51 (pointReflection_midpoint_right x y).symm52 _ = dist z y := (pointReflection ℝ (midpoint ℝ x y)).dist_map z y53 _ ≤ r := hzy54 · change dist (pointReflection ℝ (midpoint ℝ x y) z) y ≤ r55 calc56 dist (pointReflection ℝ (midpoint ℝ x y) z) y =57 dist (pointReflection ℝ (midpoint ℝ x y) z)58 (pointReflection ℝ (midpoint ℝ x y) x) :=59 congrArg (dist (pointReflection ℝ (midpoint ℝ x y) z))60 (pointReflection_midpoint_left x y).symm61 _ = dist z x := (pointReflection ℝ (midpoint ℝ x y)).dist_map z x62 _ ≤ r := hzx6364namespace IsometryEquiv6566/-- An isometry between corresponding bounded symmetric lenses maps the67midpoint of their foci to the midpoint of the target foci. -/68theorem map_midpoint_of_symmetricLens69 {x y : E} {x' y' : F} {r : ℝ}70 (hxy : 2⁻¹ * dist x y ≤ r) (hxy' : 2⁻¹ * dist x' y' ≤ r)71 (f : symmetricLens x y r ≃ᵢ symmetricLens x' y' r) :72 ((f ⟨midpoint ℝ x y, midpoint_mem_symmetricLens hxy⟩ :73 symmetricLens x' y' r) : F) = midpoint ℝ x' y' := by74 have hs : IsBounded (symmetricLens x y r) :=75 isBounded_closedBall.subset inter_subset_left76 have h := MathlibAnnex.IsometryEquiv.map_center_of_reflectionInvariant77 f (midpoint_mem_symmetricLens hxy) (midpoint_mem_symmetricLens hxy') hs78 (symmetricLens_reflectionInvariant x y r)79 (symmetricLens_reflectionInvariant x' y' r)80 exact congrArg Subtype.val h8182private def restrictToSymmetricLens83 {s : Set E} {t : Set F} (f : s ≃ᵢ t) (x y : s) (r : ℝ)84 (hs : symmetricLens (x : E) (y : E) r ⊆ s)85 (ht : symmetricLens ((f x : t) : F) ((f y : t) : F) r ⊆ t) :86 symmetricLens (x : E) (y : E) r ≃ᵢ87 symmetricLens ((f x : t) : F) ((f y : t) : F) r where88 toFun z := by89 let zs : s := ⟨z, hs z.property⟩90 refine ⟨(f zs : t), ?_⟩91 constructor92 · change dist (f zs) (f x) ≤ r93 rw [f.dist_eq, Subtype.dist_eq]94 exact z.property.195 · change dist (f zs) (f y) ≤ r96 rw [f.dist_eq, Subtype.dist_eq]97 exact z.property.298 invFun z := by99 let zt : t := ⟨z, ht z.property⟩100 refine ⟨(f.symm zt : s), ?_⟩101 constructor102 · change dist (f.symm zt) x ≤ r103 rw [← f.dist_eq, f.apply_symm_apply, Subtype.dist_eq]104 exact z.property.1105 · change dist (f.symm zt) y ≤ r106 rw [← f.dist_eq, f.apply_symm_apply, Subtype.dist_eq]107 exact z.property.2108 left_inv z := by109 apply Subtype.ext110 change ((f.symm (f ⟨(z : E), hs z.property⟩) : s) : E) = (z : E)111 exact congrArg Subtype.val (f.symm_apply_apply ⟨(z : E), hs z.property⟩)112 right_inv z := by113 apply Subtype.ext114 change ((f (f.symm ⟨(z : F), ht z.property⟩) : t) : F) = (z : F)115 exact congrArg Subtype.val (f.apply_symm_apply ⟨(z : F), ht z.property⟩)116 isometry_toFun := Isometry.of_dist_eq fun z w => by117 change dist (f ⟨z, hs z.property⟩) (f ⟨w, hs w.property⟩) = dist z w118 rw [f.dist_eq, Subtype.dist_eq, Subtype.dist_eq]119120/-- A set isometry preserves the midpoint of two points whenever the121corresponding symmetric lenses stay inside the source and target sets. -/122theorem map_midpoint_of_symmetricLens_subset123 {s : Set E} {t : Set F} (f : s ≃ᵢ t) (x y : s) (r : ℝ)124 (hhalf : 2⁻¹ * dist (x : E) (y : E) ≤ r)125 (hs : symmetricLens (x : E) (y : E) r ⊆ s)126 (ht : symmetricLens ((f x : t) : F) ((f y : t) : F) r ⊆ t) :127 ((f ⟨midpoint ℝ (x : E) (y : E),128 hs (midpoint_mem_symmetricLens hhalf)⟩ : t) : F) =129 midpoint ℝ ((f x : t) : F) ((f y : t) : F) := by130 let g := restrictToSymmetricLens f x y r hs ht131 have hdist : dist ((f x : t) : F) ((f y : t) : F) = dist (x : E) (y : E) := by132 simpa only [Subtype.dist_eq] using f.dist_eq x y133 have hhalf' : 2⁻¹ * dist ((f x : t) : F) ((f y : t) : F) ≤ r := by134 rwa [hdist]135 exact map_midpoint_of_symmetricLens hhalf hhalf' g136137/-- If corresponding ambient balls lie in the source and target sets, then a138set isometry preserves midpoints on the concentric quarter ball. -/139theorem map_midpoint_of_mem_ball140 {s : Set E} {t : Set F} (f : s ≃ᵢ t) (c : s) {R : ℝ} (hR : 0 < R)141 (hsball : ball (c : E) R ⊆ s)142 (htball : ball ((f c : t) : F) R ⊆ t)143 (x y : s) (hx : (x : E) ∈ ball (c : E) (R / 4))144 (hy : (y : E) ∈ ball (c : E) (R / 4)) :145 ((f ⟨midpoint ℝ (x : E) (y : E),146 hsball (by147 rw [mem_ball]148 calc149 dist (midpoint ℝ (x : E) (y : E)) (c : E) ≤150 (dist (x : E) (c : E) + dist (y : E) (c : E)) / 2 := by151 simpa [dist_comm] using152 dist_midpoint_midpoint_le (x : E) (y : E) (c : E) (c : E)153 _ < R := by rw [mem_ball] at hx hy; linarith)⟩ : t) : F) =154 midpoint ℝ ((f x : t) : F) ((f y : t) : F) := by155 have hxy_lt : dist (x : E) (y : E) < R / 2 := by156 calc157 dist (x : E) (y : E) ≤ dist (x : E) (c : E) + dist (c : E) (y : E) :=158 dist_triangle _ _ _159 _ < R / 4 + R / 4 := by160 rw [mem_ball] at hx hy161 exact add_lt_add hx (by simpa [dist_comm] using hy)162 _ = R / 2 := by ring163 have hhalf : 2⁻¹ * dist (x : E) (y : E) ≤ R / 2 := by164 have := hxy_lt.le165 norm_num at ⊢166 linarith167 have hsLens : symmetricLens (x : E) (y : E) (R / 2) ⊆ s := by168 intro z hz169 apply hsball170 rw [mem_ball]171 have hzx : dist z (x : E) ≤ R / 2 := hz.1172 rw [mem_ball] at hx173 calc174 dist z (c : E) ≤ dist z (x : E) + dist (x : E) (c : E) := dist_triangle _ _ _175 _ < R / 2 + R / 4 := add_lt_add_of_le_of_lt hzx hx176 _ < R := by linarith177 have hfx : dist ((f x : t) : F) ((f c : t) : F) < R / 4 := by178 rw [← Subtype.dist_eq, f.dist_eq, Subtype.dist_eq]179 exact hx180 have htLens :181 symmetricLens ((f x : t) : F) ((f y : t) : F) (R / 2) ⊆ t := by182 intro z hz183 apply htball184 rw [mem_ball]185 have hzx : dist z ((f x : t) : F) ≤ R / 2 := hz.1186 calc187 dist z ((f c : t) : F) ≤188 dist z ((f x : t) : F) + dist ((f x : t) : F) ((f c : t) : F) :=189 dist_triangle _ _ _190 _ < R / 2 + R / 4 := add_lt_add_of_le_of_lt hzx hfx191 _ < R := by linarith192 exact map_midpoint_of_symmetricLens_subset f x y (R / 2) hhalf hsLens htLens193194private theorem map_lineMap_of_map_midpoint195 {u : Set E} (hu : Convex ℝ u) (g : u → F) (hg : Continuous g)196 (hm : ∀ x y : u,197 g ⟨midpoint ℝ (x : E) (y : E), hu.midpoint_mem x.2 y.2⟩ =198 midpoint ℝ (g x) (g y))199 (x y : u) (r : ℝ) (hr : r ∈ Icc (0 : ℝ) 1) :200 g ⟨AffineMap.lineMap (x : E) (y : E) r,201 hu.lineMap_mem x.2 y.2 hr⟩ =202 AffineMap.lineMap (g x) (g y) r := by203 let p : Icc (0 : ℝ) 1 → u := fun a ↦204 ⟨AffineMap.lineMap (x : E) (y : E) (a : ℝ),205 hu.lineMap_mem x.2 y.2 a.2⟩206 have hp : Continuous p := Continuous.subtype_mk207 (AffineMap.lineMap_continuous.comp continuous_subtype_val) _208 have hrat (q : ℚ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) :209 g (p ⟨(q : ℝ), by210 constructor211 · exact_mod_cast hq0212 · exact_mod_cast hq1⟩) =213 AffineMap.lineMap (g x) (g y) (q : ℝ) := by214 let n : ℕ := q.den215 let k : ℕ := q.num.natAbs216 have hn : 0 < n := q.den_pos217 have hnR : 0 < (n : ℝ) := by exact_mod_cast hn218 have hnum : 0 ≤ q.num := Rat.num_nonneg.mpr hq0219 have hq_cast : (q : ℝ) = (k : ℝ) / (n : ℝ) := by220 have hknumZ : (k : ℤ) = q.num := by221 dsimp [k]222 exact Int.natAbs_of_nonneg hnum223 have hknumR : (k : ℝ) = (q.num : ℝ) := by exact_mod_cast hknumZ224 rw [Rat.cast_def, hknumR]225 have hq1R : (q : ℝ) ≤ 1 := by exact_mod_cast hq1226 have hkR : (k : ℝ) ≤ (n : ℝ) := by227 rw [hq_cast, div_le_one hnR] at hq1R228 exact hq1R229 have hk : k ≤ n := by exact_mod_cast hkR230 have hcoeff {i : ℕ} (hi : i ≤ n) :231 (i : ℝ) / (n : ℝ) ∈ Icc (0 : ℝ) 1 := by232 constructor233 · positivity234 · rw [div_le_one hnR]235 exact_mod_cast hi236 let Q : ℕ → F := fun i ↦237 if hi : i ≤ n then238 g ⟨AffineMap.lineMap (x : E) (y : E) ((i : ℝ) / (n : ℝ)),239 hu.lineMap_mem x.2 y.2 (hcoeff hi)⟩240 else 0241 have hQmid : ∀ i, i + 2 ≤ n →242 Q (i + 1) = midpoint ℝ (Q i) (Q (i + 2)) := by243 intro i hi244 have hi0 : i ≤ n := by omega245 have hi1 : i + 1 ≤ n := by omega246 have hi2 : i + 2 ≤ n := hi247 let z0 : u := ⟨AffineMap.lineMap (x : E) (y : E)248 ((i : ℝ) / (n : ℝ)), hu.lineMap_mem x.2 y.2 (hcoeff hi0)⟩249 let z1 : u := ⟨AffineMap.lineMap (x : E) (y : E)250 (((i + 1 : ℕ) : ℝ) / (n : ℝ)), hu.lineMap_mem x.2 y.2 (hcoeff hi1)⟩251 let z2 : u := ⟨AffineMap.lineMap (x : E) (y : E)252 (((i + 2 : ℕ) : ℝ) / (n : ℝ)), hu.lineMap_mem x.2 y.2 (hcoeff hi2)⟩253 have hz : midpoint ℝ (z0 : E) (z2 : E) = (z1 : E) := by254 change midpoint ℝ255 (AffineMap.lineMap (x : E) (y : E) ((i : ℝ) / (n : ℝ)))256 (AffineMap.lineMap (x : E) (y : E) (((i + 2 : ℕ) : ℝ) / (n : ℝ))) =257 AffineMap.lineMap (x : E) (y : E) (((i + 1 : ℕ) : ℝ) / (n : ℝ))258 calc259 _ = AffineMap.lineMap (x : E) (y : E)260 (midpoint ℝ ((i : ℝ) / (n : ℝ))261 (((i + 2 : ℕ) : ℝ) / (n : ℝ))) :=262 ((AffineMap.lineMap (x : E) (y : E)).map_midpoint _ _).symm263 _ = _ := by264 congr 1265 simp only [midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul]266 push_cast267 field_simp268 ring269 simp only [Q, dif_pos hi0, dif_pos hi1, dif_pos hi2]270 change g z1 = midpoint ℝ (g z0) (g z2)271 simpa only [hz] using hm z0 z2272 have hformula : ∀ j, j ≤ n → Q j = Q 0 + (j : ℝ) • (Q 1 - Q 0) := by273 intro j274 induction j using Nat.twoStepInduction with275 | zero => intro _; simp276 | one => intro _; simp277 | more j hj hj1 =>278 intro hj2n279 have hj_le : j ≤ n := by omega280 have hj1_le : j + 1 ≤ n := by omega281 have hmid := hQmid j hj2n282 have hmid' := congrArg (fun z : F ↦ z + z) hmid283 rw [midpoint_add_self] at hmid'284 have hj2 : Q (j + 2) = Q (j + 1) + Q (j + 1) - Q j := by285 apply (eq_sub_iff_add_eq).2286 simpa [add_comm, add_left_comm, add_assoc] using hmid'.symm287 rw [hj2, hj hj_le, hj1 hj1_le]288 simp only [Nat.cast_add, Nat.cast_one, Nat.cast_ofNat]289 module290 have H := hformula k hk291 have Hn := hformula n le_rfl292 have Q0 : Q 0 = g x := by293 simp only [Q, dif_pos (Nat.zero_le n)]294 congr 1295 apply Subtype.ext296 simp297 have Qn : Q n = g y := by298 simp only [Q, dif_pos le_rfl]299 congr 1300 apply Subtype.ext301 simp [hn.ne']302 have Qk : Q k = g (p ⟨(q : ℝ), by303 constructor304 · exact_mod_cast hq0305 · exact_mod_cast hq1⟩) := by306 simp only [Q, dif_pos hk]307 congr 1308 apply Subtype.ext309 exact congrArg (AffineMap.lineMap (x : E) (y : E)) hq_cast.symm310 rw [Qk, Q0] at H311 rw [Qn, Q0] at Hn312 rw [AffineMap.lineMap_apply_module]313 have hn0 : (n : ℝ) ≠ 0 := by exact_mod_cast hn.ne'314 have hkn : ((k : ℝ) / (n : ℝ)) * (n : ℝ) = (k : ℝ) := by field_simp315 calc316 g (p ⟨(q : ℝ), by317 constructor318 · exact_mod_cast hq0319 · exact_mod_cast hq1⟩) =320 g x + (k : ℝ) • (Q 1 - g x) := H321 _ = (1 - (q : ℝ)) • g x + (q : ℝ) • g y := by322 rw [Hn, hq_cast, smul_add, smul_smul, hkn]323 module324 let C : ℝ → Icc (0 : ℝ) 1 := fun a ↦325 ⟨max 0 (min 1 a), by constructor <;> simp⟩326 have hCcont : Continuous C := Continuous.subtype_mk327 (continuous_const.max (continuous_const.min continuous_id)) _328 have hCsurj : Function.Surjective C := by329 intro a330 refine ⟨a, Subtype.ext ?_⟩331 simp [C, a.2.1, a.2.2]332 have hdense : DenseRange (C ∘ ((↑) : ℚ → ℝ)) :=333 hCsurj.denseRange.comp Rat.denseRange_cast hCcont334 let rr : Icc (0 : ℝ) 1 := ⟨r, hr⟩335 change g (p rr) = AffineMap.lineMap (g x) (g y) (rr : ℝ)336 refine hdense.induction_on rr ?_ ?_337 · exact isClosed_eq (hg.comp hp)338 (AffineMap.lineMap_continuous.comp continuous_subtype_val)339 · intro q340 let u : ℚ := max 0 (min 1 q)341 have hu0 : 0 ≤ u := le_max_left _ _342 have hu1 : u ≤ 1 := max_le zero_le_one (min_le_left _ _)343 have hCu : C (q : ℝ) =344 ⟨(u : ℝ), by345 constructor346 · exact_mod_cast hu0347 · exact_mod_cast hu1⟩ := by348 apply Subtype.ext349 simp [C, u]350 rw [Function.comp_apply, hCu]351 exact hrat u hu0 hu1352353/-- Under the same local ball hypotheses as354`map_midpoint_of_mem_ball`, the isometry preserves every point of a355segment contained in the quarter ball. -/356theorem map_lineMap_of_mem_ball357 {s : Set E} {t : Set F} (f : s ≃ᵢ t) (c : s) {R : ℝ} (hR : 0 < R)358 (hsball : ball (c : E) R ⊆ s)359 (htball : ball ((f c : t) : F) R ⊆ t)360 (x y : s) (hx : (x : E) ∈ ball (c : E) (R / 4))361 (hy : (y : E) ∈ ball (c : E) (R / 4))362 (a : ℝ) (ha : a ∈ Icc (0 : ℝ) 1) :363 ((f ⟨AffineMap.lineMap (x : E) (y : E) a,364 hsball (ball_subset_ball (by linarith : R / 4 ≤ R)365 ((convex_ball (c : E) (R / 4)).lineMap_mem hx hy ha))⟩ : t) : F) =366 AffineMap.lineMap ((f x : t) : F) ((f y : t) : F) a := by367 let u : Set E := ball (c : E) (R / 4)368 let i : u → s := fun z ↦369 ⟨z, hsball (ball_subset_ball (by linarith : R / 4 ≤ R) z.property)⟩370 let g : u → F := fun z ↦ ((f (i z) : t) : F)371 have hi : Continuous i := Continuous.subtype_mk continuous_subtype_val _372 have hg : Continuous g :=373 continuous_subtype_val.comp (f.continuous.comp hi)374 have hm : ∀ z w : u,375 g ⟨midpoint ℝ (z : E) (w : E),376 (convex_ball (c : E) (R / 4)).midpoint_mem z.2 w.2⟩ =377 midpoint ℝ (g z) (g w) := by378 intro z w379 have h := map_midpoint_of_mem_ball f c hR hsball htball380 (i z) (i w) z.property w.property381 simpa only [g, i] using h382 let xu : u := ⟨x, hx⟩383 let yu : u := ⟨y, hy⟩384 have h := map_lineMap_of_map_midpoint385 (convex_ball (c : E) (R / 4)) g hg hm xu yu a ha386 simpa only [g, i, xu, yu] using h387388private def radialSourcePoint (c : E) (r : ℝ) (x : E) : E :=389 c + (r / ‖x‖) • x390391private theorem dist_radialSourcePoint {c : E} {r : ℝ} (hr : 0 < r)392 {x : E} (hx : x ≠ 0) : dist (radialSourcePoint c r x) c = r := by393 rw [radialSourcePoint, dist_eq_norm, add_sub_cancel_left, norm_smul,394 Real.norm_eq_abs, abs_of_pos (div_pos hr (norm_pos_iff.mpr hx))]395 field_simp396397private theorem radialSourcePoint_mem_ball {c : E} {r R : ℝ} (hr : 0 < r)398 (hrR : r < R) {x : E} (hx : x ≠ 0) : radialSourcePoint c r x ∈ ball c R := by399 rw [mem_ball, dist_radialSourcePoint hr hx]400 exact hrR401402private noncomputable def radialMap403 {s : Set E} {t : Set F} (f : s ≃ᵢ t) (c : s) (r R : ℝ)404 (hr : 0 < r) (hrR : r < R) (hsball : ball (c : E) R ⊆ s) : E → F := by405 classical406 exact fun x ↦ if hx : x = 0 then 0 else407 (‖x‖ / r) •408 (((f ⟨radialSourcePoint (c : E) r x,409 hsball (radialSourcePoint_mem_ball hr hrR hx)⟩ : t) : F) - ((f c : t) : F))410411@[simp] private theorem radialMap_zero412 {s : Set E} {t : Set F} (f : s ≃ᵢ t) (c : s) (r R : ℝ)413 (hr : 0 < r) (hrR : r < R) (hsball : ball (c : E) R ⊆ s) :414 radialMap f c r R hr hrR hsball 0 = 0 := by415 simp [radialMap]416417private theorem radialSourcePoint_smul_of_pos {c : E} {r a : ℝ}418 (ha : 0 < a) {x : E} (hx : x ≠ 0) :419 radialSourcePoint c r (a • x) = radialSourcePoint c r x := by420 have hnx : ‖x‖ ≠ 0 := (norm_pos_iff.mpr hx).ne'421 rw [radialSourcePoint, radialSourcePoint, norm_smul, Real.norm_eq_abs,422 abs_of_pos ha, smul_smul]423 congr 1424 field_simp425426private theorem radialSourcePoint_neg {c : E} {r : ℝ} {x : E} :427 radialSourcePoint c r (-x) = c - (r / ‖x‖) • x := by428 simp [radialSourcePoint, sub_eq_add_neg]429430private theorem radialMap_smul_of_pos431 {s : Set E} {t : Set F} (f : s ≃ᵢ t) (c : s) (r R : ℝ)432 (hr : 0 < r) (hrR : r < R) (hsball : ball (c : E) R ⊆ s)433 {a : ℝ} (ha : 0 < a) (x : E) :434 radialMap f c r R hr hrR hsball (a • x) =435 a • radialMap f c r R hr hrR hsball x := by436 by_cases hx : x = 0437 · subst x438 simp439 have hax : a • x ≠ 0 := smul_ne_zero ha.ne' hx440 simp only [radialMap, dif_neg hax, dif_neg hx]441 have hfpoint :442 ((f ⟨radialSourcePoint (c : E) r (a • x),443 hsball (radialSourcePoint_mem_ball hr hrR hax)⟩ : t) : F) =444 ((f ⟨radialSourcePoint (c : E) r x,445 hsball (radialSourcePoint_mem_ball hr hrR hx)⟩ : t) : F) := by446 apply congrArg Subtype.val447 apply congrArg f448 apply Subtype.ext449 exact radialSourcePoint_smul_of_pos ha hx450 rw [hfpoint, norm_smul, Real.norm_eq_abs, abs_of_pos ha, smul_smul]451 congr 1452 ring453454private theorem radialMap_neg455 {s : Set E} {t : Set F} (f : s ≃ᵢ t) (c : s) (r R : ℝ)456 (hr : 0 < r) (hrR : r < R) (hR : 0 < R) (hrq : r < R / 4)457 (hsball : ball (c : E) R ⊆ s)458 (htball : ball ((f c : t) : F) R ⊆ t) (x : E) :459 radialMap f c r R hr hrR hsball (-x) =460 -radialMap f c r R hr hrR hsball x := by461 by_cases hx : x = 0462 · subst x463 simp464 have hnx : -x ≠ 0 := neg_ne_zero.mpr hx465 let px : s := ⟨radialSourcePoint (c : E) r x,466 hsball (radialSourcePoint_mem_ball hr hrR hx)⟩467 let nx : s := ⟨radialSourcePoint (c : E) r (-x),468 hsball (radialSourcePoint_mem_ball hr hrR hnx)⟩469 have hpx : (px : E) ∈ ball (c : E) (R / 4) := by470 rw [mem_ball]471 exact (dist_radialSourcePoint hr hx).trans_lt hrq472 have hnx' : (nx : E) ∈ ball (c : E) (R / 4) := by473 rw [mem_ball]474 exact (dist_radialSourcePoint hr hnx).trans_lt hrq475 have hsource : midpoint ℝ (px : E) (nx : E) = (c : E) := by476 change midpoint ℝ (radialSourcePoint (c : E) r x)477 (radialSourcePoint (c : E) r (-x)) = (c : E)478 rw [radialSourcePoint, radialSourcePoint_neg]479 simp only [midpoint_eq_smul_add, invOf_eq_inv]480 module481 have hm := map_midpoint_of_mem_ball f c hR hsball htball482 px nx hpx hnx'483 have hfc : ((f c : t) : F) =484 midpoint ℝ ((f px : t) : F) ((f nx : t) : F) := by485 rw [← hm]486 congr 2487 apply Subtype.ext488 exact hsource.symm489 have hdiff : ((f nx : t) : F) - ((f c : t) : F) =490 -(((f px : t) : F) - ((f c : t) : F)) := by491 rw [hfc]492 simp only [midpoint_eq_smul_add, invOf_eq_inv]493 module494 simp only [radialMap, dif_neg hnx, dif_neg hx]495 rw [norm_neg]496 change (‖x‖ / r) • (((f nx : t) : F) - ((f c : t) : F)) =497 -((‖x‖ / r) • (((f px : t) : F) - ((f c : t) : F)))498 rw [hdiff]499 module500501private theorem norm_radialMap502 {s : Set E} {t : Set F} (f : s ≃ᵢ t) (c : s) (r R : ℝ)503 (hr : 0 < r) (hrR : r < R) (hsball : ball (c : E) R ⊆ s)504 (x : E) : ‖radialMap f c r R hr hrR hsball x‖ = ‖x‖ := by505 by_cases hx : x = 0506 · subst x507 simp508 rw [radialMap, dif_neg hx, norm_smul, Real.norm_eq_abs,509 abs_of_nonneg (div_nonneg (norm_nonneg x) hr.le)]510 have hd :511 ‖((f ⟨radialSourcePoint (c : E) r x,512 hsball (radialSourcePoint_mem_ball hr hrR hx)⟩ : t) : F) -513 ((f c : t) : F)‖ = r := by514 rw [← dist_eq_norm, ← Subtype.dist_eq, f.dist_eq, Subtype.dist_eq,515 dist_radialSourcePoint hr hx]516 rw [hd]517 field_simp518519private theorem map_midpoint_of_local_of_smul_pos (T : E → F) {r : ℝ} (hr : 0 < r)520 (hsmul : ∀ (a : ℝ), 0 < a → ∀ x, T (a • x) = a • T x)521 (hlocal : ∀ x y, ‖x‖ < r → ‖y‖ < r →522 T (midpoint ℝ x y) = midpoint ℝ (T x) (T y)) :523 ∀ x y, T (midpoint ℝ x y) = midpoint ℝ (T x) (T y) := by524 intro x y525 let d : ℝ := ‖x‖ + ‖y‖ + 1526 let q : ℝ := r / d527 have hd : 0 < d := by dsimp [d]; positivity528 have hq : 0 < q := div_pos hr hd529 have hqx : ‖q • x‖ < r := by530 rw [norm_smul, Real.norm_eq_abs, abs_of_pos hq]531 have hxlt : ‖x‖ < d := by dsimp [d]; linarith [norm_nonneg y]532 calc533 q * ‖x‖ < q * d := mul_lt_mul_of_pos_left hxlt hq534 _ = r := by dsimp [q]; field_simp535 have hqy : ‖q • y‖ < r := by536 rw [norm_smul, Real.norm_eq_abs, abs_of_pos hq]537 have hylt : ‖y‖ < d := by dsimp [d]; linarith [norm_nonneg x]538 calc539 q * ‖y‖ < q * d := mul_lt_mul_of_pos_left hylt hq540 _ = r := by dsimp [q]; field_simp541 have h := hlocal (q • x) (q • y) hqx hqy542 have hmid : midpoint ℝ (q • x) (q • y) = q • midpoint ℝ x y := by543 simp only [midpoint_eq_smul_add, invOf_eq_inv, smul_add, smul_smul]544 module545 rw [hmid, hsmul q hq, hsmul q hq, hsmul q hq] at h546 have hc := congrArg (fun z : F ↦ q⁻¹ • z) h547 have hcoeff : q⁻¹ * ((2 : ℝ)⁻¹ * q) = (2 : ℝ)⁻¹ := by field_simp548 simpa only [smul_smul, inv_mul_cancel₀ hq.ne', one_smul,549 midpoint_eq_smul_add, invOf_eq_inv, smul_add, hcoeff] using hc550551private def midpointAddMonoidHom (T : E → F) (h0 : T 0 = 0)552 (hm : ∀ x y, T (midpoint ℝ x y) = midpoint ℝ (T x) (T y)) : E →+ F :=553 AddMonoidHom.ofMapMidpoint ℝ ℝ T h0 hm554555@[simp] private theorem coe_midpointAddMonoidHom (T : E → F) (h0) (hm) :556 ⇑(midpointAddMonoidHom T h0 hm) = T := rfl557558private theorem midpointAddMonoidHom_isometry (T : E → F) (h0 : T 0 = 0)559 (hm : ∀ x y, T (midpoint ℝ x y) = midpoint ℝ (T x) (T y))560 (hnorm : ∀ x, ‖T x‖ = ‖x‖) : Isometry T := by561 rw [isometry_iff_dist_eq]562 intro x y563 rw [dist_eq_norm]564 have hsub := (midpointAddMonoidHom T h0 hm).map_sub x y565 change T (x - y) = T x - T y at hsub566 rw [← hsub, hnorm, ← dist_eq_norm]567568private noncomputable def midpointLinearIsometry (T : E → F) (h0 : T 0 = 0)569 (hm : ∀ x y, T (midpoint ℝ x y) = midpoint ℝ (T x) (T y))570 (hnorm : ∀ x, ‖T x‖ = ‖x‖) : E →ₗᵢ[ℝ] F :=571 { (midpointAddMonoidHom T h0 hm).toRealLinearMap572 (midpointAddMonoidHom_isometry T h0 hm hnorm).continuous with573 norm_map' := hnorm }574575@[simp] private theorem coe_midpointLinearIsometry (T : E → F) (h0) (hm) (hnorm) :576 ⇑(midpointLinearIsometry T h0 hm hnorm) = T := rfl577578private theorem radialMap_eq_sub_of_norm_lt579 {s : Set E} {t : Set F} (f : s ≃ᵢ t) (c : s) (r R : ℝ)580 (hr : 0 < r) (hrR : r < R) (hR : 0 < R) (hrq : r < R / 4)581 (hsball : ball (c : E) R ⊆ s)582 (htball : ball ((f c : t) : F) R ⊆ t)583 (x : E) (hxnorm : ‖x‖ < r) :584 radialMap f c r R hr hrR hsball x =585 ((f ⟨(c : E) + x, hsball (by586 rw [mem_ball, dist_eq_norm, add_sub_cancel_left]587 exact hxnorm.trans hrR)⟩ : t) : F) - ((f c : t) : F) := by588 let cx : s := ⟨(c : E) + x, hsball (by589 rw [mem_ball, dist_eq_norm, add_sub_cancel_left]590 exact hxnorm.trans hrR)⟩591 by_cases hx : x = 0592 · subst x593 simp594 let p : s := ⟨radialSourcePoint (c : E) r x,595 hsball (radialSourcePoint_mem_ball hr hrR hx)⟩596 have hcq : (c : E) ∈ ball (c : E) (R / 4) := by597 rw [mem_ball, dist_self]598 linarith599 have hpq : (p : E) ∈ ball (c : E) (R / 4) := by600 rw [mem_ball]601 exact (dist_radialSourcePoint hr hx).trans_lt hrq602 let a : ℝ := ‖x‖ / r603 have ha : a ∈ Icc (0 : ℝ) 1 := by604 constructor605 · exact div_nonneg (norm_nonneg x) hr.le606 · rw [div_le_one hr]607 exact hxnorm.le608 have hcoef : a * (r / ‖x‖) = 1 := by609 dsimp [a]610 field_simp [hr.ne', (norm_pos_iff.mpr hx).ne']611 have harg : AffineMap.lineMap (c : E) (p : E) a = (cx : E) := by612 change AffineMap.lineMap (c : E) (radialSourcePoint (c : E) r x) a =613 (c : E) + x614 rw [AffineMap.lineMap_apply_module, radialSourcePoint, smul_add, smul_smul,615 hcoef, one_smul]616 module617 have hline := map_lineMap_of_mem_ball f c hR hsball htball618 c p hcq hpq a ha619 have hinput :620 (⟨AffineMap.lineMap (c : E) (p : E) a,621 hsball (ball_subset_ball (by linarith : R / 4 ≤ R)622 ((convex_ball (c : E) (R / 4)).lineMap_mem hcq hpq ha))⟩ : s) = cx := by623 apply Subtype.ext624 exact harg625 rw [hinput] at hline626 simp only [radialMap, dif_neg hx]627 change a • (((f p : t) : F) - ((f c : t) : F)) =628 ((f cx : t) : F) - ((f c : t) : F)629 rw [hline, AffineMap.lineMap_apply_module]630 module631632private theorem radialMap_midpoint_of_norm_lt633 {s : Set E} {t : Set F} (f : s ≃ᵢ t) (c : s) (r R : ℝ)634 (hr : 0 < r) (hrR : r < R) (hR : 0 < R) (hrq : r < R / 4)635 (hsball : ball (c : E) R ⊆ s)636 (htball : ball ((f c : t) : F) R ⊆ t)637 (x y : E) (hx : ‖x‖ < r) (hy : ‖y‖ < r) :638 radialMap f c r R hr hrR hsball (midpoint ℝ x y) =639 midpoint ℝ (radialMap f c r R hr hrR hsball x)640 (radialMap f c r R hr hrR hsball y) := by641 have hxb : x ∈ ball (0 : E) r := by simpa [mem_ball] using hx642 have hyb : y ∈ ball (0 : E) r := by simpa [mem_ball] using hy643 have hmb : midpoint ℝ x y ∈ ball (0 : E) r :=644 (convex_ball (0 : E) r).midpoint_mem hxb hyb645 have hmnorm : ‖midpoint ℝ x y‖ < r := by simpa [mem_ball] using hmb646 let xs : s := ⟨(c : E) + x, hsball (by647 rw [mem_ball, dist_eq_norm, add_sub_cancel_left]648 exact hx.trans hrR)⟩649 let ys : s := ⟨(c : E) + y, hsball (by650 rw [mem_ball, dist_eq_norm, add_sub_cancel_left]651 exact hy.trans hrR)⟩652 let ms : s := ⟨(c : E) + midpoint ℝ x y, hsball (by653 rw [mem_ball, dist_eq_norm, add_sub_cancel_left]654 exact hmnorm.trans hrR)⟩655 have hxsq : (xs : E) ∈ ball (c : E) (R / 4) := by656 rw [mem_ball]657 change dist ((c : E) + x) (c : E) < R / 4658 rw [dist_eq_norm, add_sub_cancel_left]659 exact hx.trans hrq660 have hysq : (ys : E) ∈ ball (c : E) (R / 4) := by661 rw [mem_ball]662 change dist ((c : E) + y) (c : E) < R / 4663 rw [dist_eq_norm, add_sub_cancel_left]664 exact hy.trans hrq665 have hfm := map_midpoint_of_mem_ball f c hR hsball htball666 xs ys hxsq hysq667 have hsource : midpoint ℝ (xs : E) (ys : E) = (ms : E) := by668 change midpoint ℝ ((c : E) + x) ((c : E) + y) =669 (c : E) + midpoint ℝ x y670 simp only [midpoint_eq_smul_add, invOf_eq_inv, smul_add]671 module672 have hinput :673 (⟨midpoint ℝ (xs : E) (ys : E), hsball (by674 rw [mem_ball]675 calc676 dist (midpoint ℝ (xs : E) (ys : E)) (c : E) ≤677 (dist (xs : E) (c : E) + dist (ys : E) (c : E)) / 2 := by678 simpa [dist_comm] using679 dist_midpoint_midpoint_le (xs : E) (ys : E) (c : E) (c : E)680 _ < R := by rw [mem_ball] at hxsq hysq; linarith)⟩ : s) = ms := by681 apply Subtype.ext682 exact hsource683 rw [hinput] at hfm684 rw [radialMap_eq_sub_of_norm_lt f c r R hr hrR hR hrq hsball htball685 (midpoint ℝ x y) hmnorm,686 radialMap_eq_sub_of_norm_lt f c r R hr hrR hR hrq hsball htball x hx,687 radialMap_eq_sub_of_norm_lt f c r R hr hrR hR hrq hsball htball y hy]688 change ((f ms : t) : F) - ((f c : t) : F) =689 midpoint ℝ (((f xs : t) : F) - ((f c : t) : F))690 (((f ys : t) : F) - ((f c : t) : F))691 rw [hfm]692 simp only [midpoint_eq_smul_add, invOf_eq_inv]693 module694695/-- An isometry between subsets that contain corresponding ambient balls has696an ambient affine-isometry extension on a smaller concentric ball. -/697theorem exists_affineExtension_eqOn_ball698 {s : Set E} {t : Set F} (f : s ≃ᵢ t) (c : s) {R : ℝ} (hR : 0 < R)699 (hsball : ball (c : E) R ⊆ s)700 (htball : ball ((f c : t) : F) R ⊆ t) :701 ∃ A : E ≃ᵃⁱ[ℝ] F, ∀ x : s,702 (x : E) ∈ ball (c : E) (R / 8) → A (x : E) = ((f x : t) : F) := by703 let r : ℝ := R / 8704 have hr : 0 < r := by dsimp [r]; linarith705 have hrR : r < R := by dsimp [r]; linarith706 have hrq : r < R / 4 := by dsimp [r]; linarith707 let T : E → F := radialMap f c r R hr hrR hsball708 have hT0 : T 0 = 0 := by simp [T]709 have hTnorm : ∀ x, ‖T x‖ = ‖x‖ := by710 intro x711 exact norm_radialMap f c r R hr hrR hsball x712 have hTmid : ∀ x y, T (midpoint ℝ x y) = midpoint ℝ (T x) (T y) :=713 map_midpoint_of_local_of_smul_pos T hr714 (fun a ha x ↦ radialMap_smul_of_pos f c r R hr hrR hsball ha x)715 (fun x y hx hy ↦716 radialMap_midpoint_of_norm_lt f c r R hr hrR hR hrq hsball htball717 x y hx hy)718 let L : E →ₗᵢ[ℝ] F := midpointLinearIsometry T hT0 hTmid hTnorm719 have hball_range : ball (0 : F) r ⊆720 ((LinearMap.range L.toLinearMap : Submodule ℝ F) : Set F) := by721 intro y hy722 rw [mem_ball] at hy723 have hynorm : ‖y‖ < r := by simpa using hy724 let yt : t := ⟨((f c : t) : F) + y, htball (by725 rw [mem_ball, dist_eq_norm, add_sub_cancel_left]726 exact hynorm.trans hrR)⟩727 let xs : s := f.symm yt728 let z : E := (xs : E) - (c : E)729 have hz : ‖z‖ < r := by730 change ‖(xs : E) - (c : E)‖ < r731 rw [← dist_eq_norm, ← Subtype.dist_eq, ← f.dist_eq, f.apply_symm_apply,732 Subtype.dist_eq]733 change dist (((f c : t) : F) + y) ((f c : t) : F) < r734 simpa [dist_eq_norm] using hynorm735 have hlocal := radialMap_eq_sub_of_norm_lt f c r R hr hrR hR hrq736 hsball htball z hz737 have hpoint :738 (⟨(c : E) + z, hsball (by739 rw [mem_ball, dist_eq_norm, add_sub_cancel_left]740 exact hz.trans hrR)⟩ : s) = xs := by741 apply Subtype.ext742 dsimp [z]743 abel744 rw [hpoint, show f xs = yt from f.apply_symm_apply yt] at hlocal745 have hTy : T z = y := by746 change radialMap f c r R hr hrR hsball z = y747 change radialMap f c r R hr hrR hsball z =748 (((f c : t) : F) + y) - ((f c : t) : F) at hlocal749 simpa using hlocal750 refine ⟨z, ?_⟩751 change L z = y752 rw [coe_midpointLinearIsometry]753 exact hTy754 have hrange_interior :755 (interior ((LinearMap.range L.toLinearMap : Submodule ℝ F) : Set F)).Nonempty := by756 refine ⟨0, mem_interior_iff_mem_nhds.2 ?_⟩757 exact Filter.mem_of_superset (ball_mem_nhds (0 : F) hr) hball_range758 have hrange_top : LinearMap.range L.toLinearMap = ⊤ :=759 Submodule.eq_top_of_nonempty_interior' (LinearMap.range L.toLinearMap) hrange_interior760 have hsurj : Function.Surjective L := LinearMap.range_eq_top.mp hrange_top761 let e : E ≃ₗᵢ[ℝ] F := LinearIsometryEquiv.ofSurjective L hsurj762 let A : E ≃ᵃⁱ[ℝ] F := AffineIsometryEquiv.mk'763 (fun x : E ↦ e (x - (c : E)) + ((f c : t) : F)) e (c : E) (by764 intro x765 simp)766 refine ⟨A, ?_⟩767 intro x hx768 have hxnorm : ‖(x : E) - (c : E)‖ < r := by769 rw [mem_ball, dist_eq_norm] at hx770 exact hx771 have hlocal := radialMap_eq_sub_of_norm_lt f c r R hr hrR hR hrq772 hsball htball ((x : E) - (c : E)) hxnorm773 have hpoint :774 (⟨(c : E) + ((x : E) - (c : E)), hsball (by775 rw [mem_ball, dist_eq_norm, add_sub_cancel_left]776 exact hxnorm.trans hrR)⟩ : s) = x := by777 apply Subtype.ext778 abel_nf779 rw [hpoint] at hlocal780 change e ((x : E) - (c : E)) + ((f c : t) : F) = ((f x : t) : F)781 change L ((x : E) - (c : E)) + ((f c : t) : F) = ((f x : t) : F)782 rw [coe_midpointLinearIsometry]783 change radialMap f c r R hr hrR hsball ((x : E) - (c : E)) +784 ((f c : t) : F) = ((f x : t) : F)785 rw [hlocal]786 abel787788end IsometryEquiv789790end791792end MathlibAnnex