MATHLIBANNEX / EXACT SOURCE v0.4.0
MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens_subset
theorem map_midpoint_of_symmetricLens_subset
{s : Set E} {t : Set F} (f : s ≃ᵢ t) (x y : s) (r : ℝ)
(hhalf : 2⁻¹ * dist (x : E) (y : E) ≤ r)
(hs : symmetricLens (x : E) (y : E) r ⊆ s)
(ht : symmetricLens ((f x : t) : F) ((f y : t) : F) r ⊆ t) :
((f ⟨midpoint ℝ (x : E) (y : E),
hs (midpoint_mem_symmetricLens hhalf)⟩ : t) : F) =
midpoint ℝ ((f x : t) : F) ((f y : t) : F)1 import MathlibAnnex.Analysis.Normed.Affine.Reflection 2 import Mathlib.Analysis.Convex.Basic 3 import Mathlib.Analysis.Normed.Affine.AddTorsor 4 import Mathlib.Analysis.Normed.Module.Convex 5 import Mathlib.LinearAlgebra.AffineSpace.MidpointZero 6 import Mathlib.Tactic.Linarith 7 import Mathlib.Tactic.Module 8 import Mathlib.Tactic.NormNum 9 import Mathlib.Tactic.Order 10 import Mathlib.Tactic.Positivity 11 import Mathlib.Tactic.Ring 12 13 /-! 14 # Local extension machinery for isometries 15 16 This module develops the local midpoint and affine-segment identities used to 17 extend isometries between open subsets of real normed spaces. 18 -/ 19 20 open Metric Set AffineIsometryEquiv Bornology 21 22 namespace MathlibAnnex 23 24 noncomputable section 25 26 variable {E F : Type*} 27 [NormedAddCommGroup E] [NormedSpace ℝ E] 28 [NormedAddCommGroup F] [NormedSpace ℝ F] 29 30 /-- The intersection of two closed balls with the same radius. -/ 31 def symmetricLens (x y : E) (r : ℝ) : Set E := 32 closedBall x r ∩ closedBall y r 33 34 private theorem midpoint_mem_symmetricLens {x y : E} {r : ℝ} 35 (h : 2⁻¹ * dist x y ≤ r) : midpoint ℝ x y ∈ symmetricLens x y r := by 36 constructor 37 · simpa [symmetricLens, dist_midpoint_left, Real.norm_two] using h 38 · simpa [symmetricLens, dist_midpoint_right, Real.norm_two] using h 39 40 private theorem mapsTo_pointReflection_symmetricLens (x y : E) (r : ℝ) : 41 MapsTo (pointReflection ℝ (midpoint ℝ x y)) 42 (symmetricLens x y r) (symmetricLens x y r) := by 43 rintro z ⟨hzx, hzy⟩ 44 constructor 45 · change dist (pointReflection ℝ (midpoint ℝ x y) z) x ≤ r 46 calc 47 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).symm 52 _ = dist z y := (pointReflection ℝ (midpoint ℝ x y)).dist_map z y 53 _ ≤ r := hzy 54 · change dist (pointReflection ℝ (midpoint ℝ x y) z) y ≤ r 55 calc 56 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).symm 61 _ = dist z x := (pointReflection ℝ (midpoint ℝ x y)).dist_map z x 62 _ ≤ r := hzx 63 64 namespace IsometryEquiv 65 66 /-- An isometry between corresponding bounded symmetric lenses maps the 67 midpoint of their foci to the midpoint of the target foci. -/ 68 theorem map_midpoint_of_symmetricLens 69 {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' := by 74 have hs : IsBounded (symmetricLens x y r) := 75 isBounded_closedBall.subset inter_subset_left 76 have h := MathlibAnnex.IsometryEquiv.map_center_of_mapsTo_pointReflection 77 f (midpoint_mem_symmetricLens hxy) (midpoint_mem_symmetricLens hxy') hs 78 (mapsTo_pointReflection_symmetricLens x y r) 79 (mapsTo_pointReflection_symmetricLens x' y' r) 80 exact congrArg Subtype.val h 81 82 private def restrictToSymmetricLens 83 {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 where 88 toFun z := by 89 let zs : s := ⟨z, hs z.property⟩ 90 refine ⟨(f zs : t), ?_⟩ 91 constructor 92 · change dist (f zs) (f x) ≤ r 93 rw [f.dist_eq, Subtype.dist_eq] 94 exact z.property.1 95 · change dist (f zs) (f y) ≤ r 96 rw [f.dist_eq, Subtype.dist_eq] 97 exact z.property.2 98 invFun z := by 99 let zt : t := ⟨z, ht z.property⟩ 100 refine ⟨(f.symm zt : s), ?_⟩ 101 constructor 102 · change dist (f.symm zt) x ≤ r 103 rw [← f.dist_eq, f.apply_symm_apply, Subtype.dist_eq] 104 exact z.property.1 105 · change dist (f.symm zt) y ≤ r 106 rw [← f.dist_eq, f.apply_symm_apply, Subtype.dist_eq] 107 exact z.property.2 108 left_inv z := by 109 apply Subtype.ext 110 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 := by 113 apply Subtype.ext 114 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 => by 117 change dist (f ⟨z, hs z.property⟩) (f ⟨w, hs w.property⟩) = dist z w 118 rw [f.dist_eq, Subtype.dist_eq, Subtype.dist_eq] 119 120 /-- A set isometry preserves the midpoint of two points whenever the 121 corresponding symmetric lenses stay inside the source and target sets. -/ 122 theorem map_midpoint_of_symmetricLens_subset 123 {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) := by 130 let g := restrictToSymmetricLens f x y r hs ht 131 have hdist : dist ((f x : t) : F) ((f y : t) : F) = dist (x : E) (y : E) := by 132 simpa only [Subtype.dist_eq] using f.dist_eq x y 133 have hhalf' : 2⁻¹ * dist ((f x : t) : F) ((f y : t) : F) ≤ r := by 134 rwa [hdist] 135 exact map_midpoint_of_symmetricLens hhalf hhalf' g 136 137 /-- If corresponding ambient balls lie in the source and target sets, then a 138 set isometry preserves midpoints on the concentric quarter ball. -/ 139 theorem map_midpoint_of_mem_ball 140 {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 (by 147 rw [mem_ball] 148 calc 149 dist (midpoint ℝ (x : E) (y : E)) (c : E) ≤ 150 (dist (x : E) (c : E) + dist (y : E) (c : E)) / 2 := by 151 simpa [dist_comm] using 152 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) := by 155 have hxy_lt : dist (x : E) (y : E) < R / 2 := by 156 calc 157 dist (x : E) (y : E) ≤ dist (x : E) (c : E) + dist (c : E) (y : E) := 158 dist_triangle _ _ _ 159 _ < R / 4 + R / 4 := by 160 rw [mem_ball] at hx hy 161 exact add_lt_add hx (by simpa [dist_comm] using hy) 162 _ = R / 2 := by ring 163 have hhalf : 2⁻¹ * dist (x : E) (y : E) ≤ R / 2 := by 164 have := hxy_lt.le 165 norm_num at ⊢ 166 linarith 167 have hsLens : symmetricLens (x : E) (y : E) (R / 2) ⊆ s := by 168 intro z hz 169 apply hsball 170 rw [mem_ball] 171 have hzx : dist z (x : E) ≤ R / 2 := hz.1 172 rw [mem_ball] at hx 173 calc 174 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 hx 176 _ < R := by linarith 177 have hfx : dist ((f x : t) : F) ((f c : t) : F) < R / 4 := by 178 rw [← Subtype.dist_eq, f.dist_eq, Subtype.dist_eq] 179 exact hx 180 have htLens : 181 symmetricLens ((f x : t) : F) ((f y : t) : F) (R / 2) ⊆ t := by 182 intro z hz 183 apply htball 184 rw [mem_ball] 185 have hzx : dist z ((f x : t) : F) ≤ R / 2 := hz.1 186 calc 187 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 hfx 191 _ < R := by linarith 192 exact map_midpoint_of_symmetricLens_subset f x y (R / 2) hhalf hsLens htLens 193 194 private theorem map_lineMap_of_map_midpoint 195 {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 := by 203 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_mk 207 (AffineMap.lineMap_continuous.comp continuous_subtype_val) _ 208 have hrat (q : ℚ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) : 209 g (p ⟨(q : ℝ), by 210 constructor 211 · exact_mod_cast hq0 212 · exact_mod_cast hq1⟩) = 213 AffineMap.lineMap (g x) (g y) (q : ℝ) := by 214 let n : ℕ := q.den 215 let k : ℕ := q.num.natAbs 216 have hn : 0 < n := q.den_pos 217 have hnR : 0 < (n : ℝ) := by exact_mod_cast hn 218 have hnum : 0 ≤ q.num := Rat.num_nonneg.mpr hq0 219 have hq_cast : (q : ℝ) = (k : ℝ) / (n : ℝ) := by 220 have hknumZ : (k : ℤ) = q.num := by 221 dsimp [k] 222 exact Int.natAbs_of_nonneg hnum 223 have hknumR : (k : ℝ) = (q.num : ℝ) := by exact_mod_cast hknumZ 224 rw [Rat.cast_def, hknumR] 225 have hq1R : (q : ℝ) ≤ 1 := by exact_mod_cast hq1 226 have hkR : (k : ℝ) ≤ (n : ℝ) := by 227 rw [hq_cast, div_le_one hnR] at hq1R 228 exact hq1R 229 have hk : k ≤ n := by exact_mod_cast hkR 230 have hcoeff {i : ℕ} (hi : i ≤ n) : 231 (i : ℝ) / (n : ℝ) ∈ Icc (0 : ℝ) 1 := by 232 constructor 233 · positivity 234 · rw [div_le_one hnR] 235 exact_mod_cast hi 236 let Q : ℕ → F := fun i ↦ 237 if hi : i ≤ n then 238 g ⟨AffineMap.lineMap (x : E) (y : E) ((i : ℝ) / (n : ℝ)), 239 hu.lineMap_mem x.2 y.2 (hcoeff hi)⟩ 240 else 0 241 have hQmid : ∀ i, i + 2 ≤ n → 242 Q (i + 1) = midpoint ℝ (Q i) (Q (i + 2)) := by 243 intro i hi 244 have hi0 : i ≤ n := by omega 245 have hi1 : i + 1 ≤ n := by omega 246 have hi2 : i + 2 ≤ n := hi 247 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) := by 254 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 calc 259 _ = AffineMap.lineMap (x : E) (y : E) 260 (midpoint ℝ ((i : ℝ) / (n : ℝ)) 261 (((i + 2 : ℕ) : ℝ) / (n : ℝ))) := 262 ((AffineMap.lineMap (x : E) (y : E)).map_midpoint _ _).symm 263 _ = _ := by 264 congr 1 265 simp only [midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul] 266 push_cast 267 field_simp 268 ring 269 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 z2 272 have hformula : ∀ j, j ≤ n → Q j = Q 0 + (j : ℝ) • (Q 1 - Q 0) := by 273 intro j 274 induction j using Nat.twoStepInduction with 275 | zero => intro _; simp 276 | one => intro _; simp 277 | more j hj hj1 => 278 intro hj2n 279 have hj_le : j ≤ n := by omega 280 have hj1_le : j + 1 ≤ n := by omega 281 have hmid := hQmid j hj2n 282 have hmid' := congrArg (fun z : F ↦ z + z) hmid 283 rw [midpoint_add_self] at hmid' 284 have hj2 : Q (j + 2) = Q (j + 1) + Q (j + 1) - Q j := by 285 apply (eq_sub_iff_add_eq).2 286 simpa [add_comm, add_left_comm, add_assoc] using hmid'.symm 287 rw [hj2, hj hj_le, hj1 hj1_le] 288 simp only [Nat.cast_add, Nat.cast_one, Nat.cast_ofNat] 289 module 290 have H := hformula k hk 291 have Hn := hformula n le_rfl 292 have Q0 : Q 0 = g x := by 293 simp only [Q, dif_pos (Nat.zero_le n)] 294 congr 1 295 apply Subtype.ext 296 simp 297 have Qn : Q n = g y := by 298 simp only [Q, dif_pos le_rfl] 299 congr 1 300 apply Subtype.ext 301 simp [hn.ne'] 302 have Qk : Q k = g (p ⟨(q : ℝ), by 303 constructor 304 · exact_mod_cast hq0 305 · exact_mod_cast hq1⟩) := by 306 simp only [Q, dif_pos hk] 307 congr 1 308 apply Subtype.ext 309 exact congrArg (AffineMap.lineMap (x : E) (y : E)) hq_cast.symm 310 rw [Qk, Q0] at H 311 rw [Qn, Q0] at Hn 312 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_simp 315 calc 316 g (p ⟨(q : ℝ), by 317 constructor 318 · exact_mod_cast hq0 319 · exact_mod_cast hq1⟩) = 320 g x + (k : ℝ) • (Q 1 - g x) := H 321 _ = (1 - (q : ℝ)) • g x + (q : ℝ) • g y := by 322 rw [Hn, hq_cast, smul_add, smul_smul, hkn] 323 module 324 let C : ℝ → Icc (0 : ℝ) 1 := fun a ↦ 325 ⟨max 0 (min 1 a), by constructor <;> simp⟩ 326 have hCcont : Continuous C := Continuous.subtype_mk 327 (continuous_const.max (continuous_const.min continuous_id)) _ 328 have hCsurj : Function.Surjective C := by 329 intro a 330 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 hCcont 334 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 q 340 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 : ℝ), by 345 constructor 346 · exact_mod_cast hu0 347 · exact_mod_cast hu1⟩ := by 348 apply Subtype.ext 349 simp [C, u] 350 rw [Function.comp_apply, hCu] 351 exact hrat u hu0 hu1 352 353 /-- Under the same local ball hypotheses as 354 `map_midpoint_of_mem_ball`, the isometry preserves every point of a 355 segment contained in the quarter ball. -/ 356 theorem map_lineMap_of_mem_ball 357 {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 := by 367 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) := by 378 intro z w 379 have h := map_midpoint_of_mem_ball f c hR hsball htball 380 (i z) (i w) z.property w.property 381 simpa only [g, i] using h 382 let xu : u := ⟨x, hx⟩ 383 let yu : u := ⟨y, hy⟩ 384 have h := map_lineMap_of_map_midpoint 385 (convex_ball (c : E) (R / 4)) g hg hm xu yu a ha 386 simpa only [g, i, xu, yu] using h 387 388 private def radialSourcePoint (c : E) (r : ℝ) (x : E) : E := 389 c + (r / ‖x‖) • x 390 391 private theorem dist_radialSourcePoint {c : E} {r : ℝ} (hr : 0 < r) 392 {x : E} (hx : x ≠ 0) : dist (radialSourcePoint c r x) c = r := by 393 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_simp 396 397 private 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 := by 399 rw [mem_ball, dist_radialSourcePoint hr hx] 400 exact hrR 401 402 private noncomputable def radialMap 403 {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 := by 405 classical 406 exact fun x ↦ if hx : x = 0 then 0 else 407 (‖x‖ / r) • 408 (((f ⟨radialSourcePoint (c : E) r x, 409 hsball (radialSourcePoint_mem_ball hr hrR hx)⟩ : t) : F) - ((f c : t) : F)) 410 411 @[simp] private theorem radialMap_zero 412 {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 := by 415 simp [radialMap] 416 417 private 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 := by 420 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 1 424 field_simp 425 426 private theorem radialSourcePoint_neg {c : E} {r : ℝ} {x : E} : 427 radialSourcePoint c r (-x) = c - (r / ‖x‖) • x := by 428 simp [radialSourcePoint, sub_eq_add_neg] 429 430 private theorem radialMap_smul_of_pos 431 {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 := by 436 by_cases hx : x = 0 437 · subst x 438 simp 439 have hax : a • x ≠ 0 := smul_ne_zero ha.ne' hx 440 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) := by 446 apply congrArg Subtype.val 447 apply congrArg f 448 apply Subtype.ext 449 exact radialSourcePoint_smul_of_pos ha hx 450 rw [hfpoint, norm_smul, Real.norm_eq_abs, abs_of_pos ha, smul_smul] 451 congr 1 452 ring 453 454 private theorem radialMap_neg 455 {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 := by 461 by_cases hx : x = 0 462 · subst x 463 simp 464 have hnx : -x ≠ 0 := neg_ne_zero.mpr hx 465 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) := by 470 rw [mem_ball] 471 exact (dist_radialSourcePoint hr hx).trans_lt hrq 472 have hnx' : (nx : E) ∈ ball (c : E) (R / 4) := by 473 rw [mem_ball] 474 exact (dist_radialSourcePoint hr hnx).trans_lt hrq 475 have hsource : midpoint ℝ (px : E) (nx : E) = (c : E) := by 476 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 module 481 have hm := map_midpoint_of_mem_ball f c hR hsball htball 482 px nx hpx hnx' 483 have hfc : ((f c : t) : F) = 484 midpoint ℝ ((f px : t) : F) ((f nx : t) : F) := by 485 rw [← hm] 486 congr 2 487 apply Subtype.ext 488 exact hsource.symm 489 have hdiff : ((f nx : t) : F) - ((f c : t) : F) = 490 -(((f px : t) : F) - ((f c : t) : F)) := by 491 rw [hfc] 492 simp only [midpoint_eq_smul_add, invOf_eq_inv] 493 module 494 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 module 500 501 private theorem norm_radialMap 502 {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‖ := by 505 by_cases hx : x = 0 506 · subst x 507 simp 508 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 := by 514 rw [← dist_eq_norm, ← Subtype.dist_eq, f.dist_eq, Subtype.dist_eq, 515 dist_radialSourcePoint hr hx] 516 rw [hd] 517 field_simp 518 519 private 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) := by 524 intro x y 525 let d : ℝ := ‖x‖ + ‖y‖ + 1 526 let q : ℝ := r / d 527 have hd : 0 < d := by dsimp [d]; positivity 528 have hq : 0 < q := div_pos hr hd 529 have hqx : ‖q • x‖ < r := by 530 rw [norm_smul, Real.norm_eq_abs, abs_of_pos hq] 531 have hxlt : ‖x‖ < d := by dsimp [d]; linarith [norm_nonneg y] 532 calc 533 q * ‖x‖ < q * d := mul_lt_mul_of_pos_left hxlt hq 534 _ = r := by dsimp [q]; field_simp 535 have hqy : ‖q • y‖ < r := by 536 rw [norm_smul, Real.norm_eq_abs, abs_of_pos hq] 537 have hylt : ‖y‖ < d := by dsimp [d]; linarith [norm_nonneg x] 538 calc 539 q * ‖y‖ < q * d := mul_lt_mul_of_pos_left hylt hq 540 _ = r := by dsimp [q]; field_simp 541 have h := hlocal (q • x) (q • y) hqx hqy 542 have hmid : midpoint ℝ (q • x) (q • y) = q • midpoint ℝ x y := by 543 simp only [midpoint_eq_smul_add, invOf_eq_inv, smul_add, smul_smul] 544 module 545 rw [hmid, hsmul q hq, hsmul q hq, hsmul q hq] at h 546 have hc := congrArg (fun z : F ↦ q⁻¹ • z) h 547 have hcoeff : q⁻¹ * ((2 : ℝ)⁻¹ * q) = (2 : ℝ)⁻¹ := by field_simp 548 simpa only [smul_smul, inv_mul_cancel₀ hq.ne', one_smul, 549 midpoint_eq_smul_add, invOf_eq_inv, smul_add, hcoeff] using hc 550 551 private 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 hm 554 555 @[simp] private theorem coe_midpointAddMonoidHom (T : E → F) (h0) (hm) : 556 ⇑(midpointAddMonoidHom T h0 hm) = T := rfl 557 558 private theorem isometry_midpointAddMonoidHom (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 := by 561 rw [isometry_iff_dist_eq] 562 intro x y 563 rw [dist_eq_norm] 564 have hsub := (midpointAddMonoidHom T h0 hm).map_sub x y 565 change T (x - y) = T x - T y at hsub 566 rw [← hsub, hnorm, ← dist_eq_norm] 567 568 private 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).toRealLinearMap 572 (isometry_midpointAddMonoidHom T h0 hm hnorm).continuous with 573 norm_map' := hnorm } 574 575 @[simp] private theorem coe_midpointLinearIsometry (T : E → F) (h0) (hm) (hnorm) : 576 ⇑(midpointLinearIsometry T h0 hm hnorm) = T := rfl 577 578 private theorem radialMap_eq_sub_of_norm_lt 579 {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 (by 586 rw [mem_ball, dist_eq_norm, add_sub_cancel_left] 587 exact hxnorm.trans hrR)⟩ : t) : F) - ((f c : t) : F) := by 588 let cx : s := ⟨(c : E) + x, hsball (by 589 rw [mem_ball, dist_eq_norm, add_sub_cancel_left] 590 exact hxnorm.trans hrR)⟩ 591 by_cases hx : x = 0 592 · subst x 593 simp 594 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) := by 597 rw [mem_ball, dist_self] 598 linarith 599 have hpq : (p : E) ∈ ball (c : E) (R / 4) := by 600 rw [mem_ball] 601 exact (dist_radialSourcePoint hr hx).trans_lt hrq 602 let a : ℝ := ‖x‖ / r 603 have ha : a ∈ Icc (0 : ℝ) 1 := by 604 constructor 605 · exact div_nonneg (norm_nonneg x) hr.le 606 · rw [div_le_one hr] 607 exact hxnorm.le 608 have hcoef : a * (r / ‖x‖) = 1 := by 609 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) := by 612 change AffineMap.lineMap (c : E) (radialSourcePoint (c : E) r x) a = 613 (c : E) + x 614 rw [AffineMap.lineMap_apply_module, radialSourcePoint, smul_add, smul_smul, 615 hcoef, one_smul] 616 module 617 have hline := map_lineMap_of_mem_ball f c hR hsball htball 618 c p hcq hpq a ha 619 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 := by 623 apply Subtype.ext 624 exact harg 625 rw [hinput] at hline 626 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 module 631 632 private theorem radialMap_midpoint_of_norm_lt 633 {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) := by 641 have hxb : x ∈ ball (0 : E) r := by simpa [mem_ball] using hx 642 have hyb : y ∈ ball (0 : E) r := by simpa [mem_ball] using hy 643 have hmb : midpoint ℝ x y ∈ ball (0 : E) r := 644 (convex_ball (0 : E) r).midpoint_mem hxb hyb 645 have hmnorm : ‖midpoint ℝ x y‖ < r := by simpa [mem_ball] using hmb 646 let xs : s := ⟨(c : E) + x, hsball (by 647 rw [mem_ball, dist_eq_norm, add_sub_cancel_left] 648 exact hx.trans hrR)⟩ 649 let ys : s := ⟨(c : E) + y, hsball (by 650 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 (by 653 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) := by 656 rw [mem_ball] 657 change dist ((c : E) + x) (c : E) < R / 4 658 rw [dist_eq_norm, add_sub_cancel_left] 659 exact hx.trans hrq 660 have hysq : (ys : E) ∈ ball (c : E) (R / 4) := by 661 rw [mem_ball] 662 change dist ((c : E) + y) (c : E) < R / 4 663 rw [dist_eq_norm, add_sub_cancel_left] 664 exact hy.trans hrq 665 have hfm := map_midpoint_of_mem_ball f c hR hsball htball 666 xs ys hxsq hysq 667 have hsource : midpoint ℝ (xs : E) (ys : E) = (ms : E) := by 668 change midpoint ℝ ((c : E) + x) ((c : E) + y) = 669 (c : E) + midpoint ℝ x y 670 simp only [midpoint_eq_smul_add, invOf_eq_inv, smul_add] 671 module 672 have hinput : 673 (⟨midpoint ℝ (xs : E) (ys : E), hsball (by 674 rw [mem_ball] 675 calc 676 dist (midpoint ℝ (xs : E) (ys : E)) (c : E) ≤ 677 (dist (xs : E) (c : E) + dist (ys : E) (c : E)) / 2 := by 678 simpa [dist_comm] using 679 dist_midpoint_midpoint_le (xs : E) (ys : E) (c : E) (c : E) 680 _ < R := by rw [mem_ball] at hxsq hysq; linarith)⟩ : s) = ms := by 681 apply Subtype.ext 682 exact hsource 683 rw [hinput] at hfm 684 rw [radialMap_eq_sub_of_norm_lt f c r R hr hrR hR hrq hsball htball 685 (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 module 694 695 /-- An isometry between subsets that contain corresponding ambient balls has 696 an ambient affine-isometry extension on a smaller concentric ball. -/ 697 theorem exists_affineExtension_eqOn_ball 698 {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) := by 703 let r : ℝ := R / 8 704 have hr : 0 < r := by dsimp [r]; linarith 705 have hrR : r < R := by dsimp [r]; linarith 706 have hrq : r < R / 4 := by dsimp [r]; linarith 707 let T : E → F := radialMap f c r R hr hrR hsball 708 have hT0 : T 0 = 0 := by simp [T] 709 have hTnorm : ∀ x, ‖T x‖ = ‖x‖ := by 710 intro x 711 exact norm_radialMap f c r R hr hrR hsball x 712 have hTmid : ∀ x y, T (midpoint ℝ x y) = midpoint ℝ (T x) (T y) := 713 map_midpoint_of_local_of_smul_pos T hr 714 (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 htball 717 x y hx hy) 718 let L : E →ₗᵢ[ℝ] F := midpointLinearIsometry T hT0 hTmid hTnorm 719 have hball_range : ball (0 : F) r ⊆ 720 ((LinearMap.range L.toLinearMap : Submodule ℝ F) : Set F) := by 721 intro y hy 722 rw [mem_ball] at hy 723 have hynorm : ‖y‖ < r := by simpa using hy 724 let yt : t := ⟨((f c : t) : F) + y, htball (by 725 rw [mem_ball, dist_eq_norm, add_sub_cancel_left] 726 exact hynorm.trans hrR)⟩ 727 let xs : s := f.symm yt 728 let z : E := (xs : E) - (c : E) 729 have hz : ‖z‖ < r := by 730 change ‖(xs : E) - (c : E)‖ < r 731 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) < r 734 simpa [dist_eq_norm] using hynorm 735 have hlocal := radialMap_eq_sub_of_norm_lt f c r R hr hrR hR hrq 736 hsball htball z hz 737 have hpoint : 738 (⟨(c : E) + z, hsball (by 739 rw [mem_ball, dist_eq_norm, add_sub_cancel_left] 740 exact hz.trans hrR)⟩ : s) = xs := by 741 apply Subtype.ext 742 dsimp [z] 743 abel 744 rw [hpoint, show f xs = yt from f.apply_symm_apply yt] at hlocal 745 have hTy : T z = y := by 746 change radialMap f c r R hr hrR hsball z = y 747 change radialMap f c r R hr hrR hsball z = 748 (((f c : t) : F) + y) - ((f c : t) : F) at hlocal 749 simpa using hlocal 750 refine ⟨z, ?_⟩ 751 change L z = y 752 rw [coe_midpointLinearIsometry] 753 exact hTy 754 have hrange_interior : 755 (interior ((LinearMap.range L.toLinearMap : Submodule ℝ F) : Set F)).Nonempty := by 756 refine ⟨0, mem_interior_iff_mem_nhds.2 ?_⟩ 757 exact Filter.mem_of_superset (ball_mem_nhds (0 : F) hr) hball_range 758 have hrange_top : LinearMap.range L.toLinearMap = ⊤ := 759 Submodule.eq_top_of_nonempty_interior' (LinearMap.range L.toLinearMap) hrange_interior 760 have hsurj : Function.Surjective L := LinearMap.range_eq_top.mp hrange_top 761 let e : E ≃ₗᵢ[ℝ] F := LinearIsometryEquiv.ofSurjective L hsurj 762 let A : E ≃ᵃⁱ[ℝ] F := AffineIsometryEquiv.mk' 763 (fun x : E ↦ e (x - (c : E)) + ((f c : t) : F)) e (c : E) (by 764 intro x 765 simp) 766 refine ⟨A, ?_⟩ 767 intro x hx 768 have hxnorm : ‖(x : E) - (c : E)‖ < r := by 769 rw [mem_ball, dist_eq_norm] at hx 770 exact hx 771 have hlocal := radialMap_eq_sub_of_norm_lt f c r R hr hrR hR hrq 772 hsball htball ((x : E) - (c : E)) hxnorm 773 have hpoint : 774 (⟨(c : E) + ((x : E) - (c : E)), hsball (by 775 rw [mem_ball, dist_eq_norm, add_sub_cancel_left] 776 exact hxnorm.trans hrR)⟩ : s) = x := by 777 apply Subtype.ext 778 abel_nf 779 rw [hpoint] at hlocal 780 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 abel 787 788 end IsometryEquiv 789 790 end 791 792 end MathlibAnnex