MATHLIBANNEX / EXACT SOURCE v0.4.0
MathlibAnnex.IsometryEquiv.existsUnique_affineExtension
theorem existsUnique_affineExtension
{s : Set E} {t : Set F} (f : s ≃ᵢ t)
(hs : IsOpen s) (hsc : IsConnected s) (ht : IsOpen t) :
∃! A : E ≃ᵃⁱ[ℝ] F,
∀ x : s, A (x : E) = ((f x : t) : F)1 import MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Local 2 import Mathlib.Topology.LocallyConstant.Basic 3 4 /-! 5 # Extension from open connected domains 6 7 This module glues the local affine-isometry extensions into a unique ambient 8 affine isometry equivalence. 9 -/ 10 11 open Metric Set AffineIsometryEquiv 12 13 namespace MathlibAnnex 14 15 noncomputable section 16 17 variable {E F : Type*} 18 [NormedAddCommGroup E] [NormedSpace ℝ E] 19 [NormedAddCommGroup F] [NormedSpace ℝ F] 20 21 namespace IsometryEquiv 22 23 private theorem affineIsometryEquiv_map_lineMap 24 (A : E ≃ᵃⁱ[ℝ] F) (c x : E) (a : ℝ) : 25 A (AffineMap.lineMap c x a) = 26 AffineMap.lineMap (A c) (A x) a := by 27 rw [AffineMap.lineMap_apply_module', AffineMap.lineMap_apply_module'] 28 change A.toAffineEquiv.toAffineMap (a • (x - c) + c) = _ 29 rw [show a • (x - c) + c = a • (x - c) +ᵥ c by rfl] 30 rw [AffineMap.map_vadd] 31 change A.toAffineEquiv.toAffineMap.linear (a • (x -ᵥ c)) +ᵥ A c = 32 a • (A x -ᵥ A c) +ᵥ A c 33 rw [LinearMap.map_smul, A.toAffineEquiv.toAffineMap.linearMap_vsub] 34 rfl 35 36 private theorem affineIsometryEquiv_eq_of_isOpen_of_eqOn 37 {u : Set E} (hu : IsOpen u) (hne : u.Nonempty) 38 (A B : E ≃ᵃⁱ[ℝ] F) (h : u.EqOn A B) : A = B := by 39 rcases hne with ⟨c, hc⟩ 40 rcases Metric.mem_nhds_iff.1 (hu.mem_nhds hc) with ⟨ε, hε, hball⟩ 41 apply AffineIsometryEquiv.ext 42 intro x 43 by_cases hxc : x = c 44 · subst x 45 exact h hc 46 let a : ℝ := ε / (2 * dist x c) 47 have hd : 0 < dist x c := dist_pos.mpr hxc 48 have ha : 0 < a := div_pos hε (mul_pos (by norm_num) hd) 49 let y : E := AffineMap.lineMap c x a 50 have hyc : dist y c = ε / 2 := by 51 simp only [y] 52 rw [AffineMap.lineMap_apply_module', dist_eq_norm, 53 add_sub_cancel_right, norm_smul, Real.norm_eq_abs, 54 abs_of_pos ha, ← dist_eq_norm] 55 simp only [a] 56 field_simp 57 have hy : y ∈ u := by 58 apply hball 59 rw [mem_ball, hyc] 60 linarith 61 have hcAB : A c = B c := h hc 62 have hyAB : A y = B y := h hy 63 have hline : AffineMap.lineMap (A c) (A x) a = 64 AffineMap.lineMap (B c) (B x) a := by 65 rw [← affineIsometryEquiv_map_lineMap A c x a, 66 ← affineIsometryEquiv_map_lineMap B c x a] 67 exact hyAB 68 rw [AffineMap.lineMap_apply_module', AffineMap.lineMap_apply_module', hcAB] at hline 69 have hv : A x - B c = B x - B c := by 70 apply smul_right_injective F ha.ne' 71 exact add_right_cancel hline 72 exact sub_left_injective hv 73 74 private theorem existsUnique_affineIsometryEquiv_of_local 75 {s : Set E} (hs : IsOpen s) (hsc : IsConnected s) (f : s → F) 76 (hlocal : ∀ x : s, ∃ A : E ≃ᵃⁱ[ℝ] F, ∃ r > 0, 77 ∀ y : s, dist (y : E) (x : E) < r → A (y : E) = f y) : 78 ∃! A : E ≃ᵃⁱ[ℝ] F, ∀ x : s, A (x : E) = f x := by 79 let chart : s → E ≃ᵃⁱ[ℝ] F := fun x ↦ Classical.choose (hlocal x) 80 have chart_spec (x : s) : ∃ r > 0, 81 ∀ y : s, dist (y : E) (x : E) < r → chart x (y : E) = f y := 82 Classical.choose_spec (hlocal x) 83 have hchart : IsLocallyConstant chart := by 84 rw [IsLocallyConstant.iff_eventually_eq] 85 intro x 86 rcases chart_spec x with ⟨r, hr, hxr⟩ 87 filter_upwards [ball_mem_nhds x hr] with y hy 88 rcases chart_spec y with ⟨q, hq, hyq⟩ 89 let u : Set E := (s ∩ ball (x : E) r) ∩ ball (y : E) q 90 have hu : IsOpen u := (hs.inter isOpen_ball).inter isOpen_ball 91 have hyx : dist (y : E) (x : E) < r := by 92 simpa only [mem_ball, Subtype.dist_eq] using hy 93 have hune : u.Nonempty := by 94 refine ⟨(y : E), ⟨y.property, ?_⟩, mem_ball_self hq⟩ 95 exact hyx 96 have heq : u.EqOn (chart y) (chart x) := by 97 intro z hz 98 let zs : s := ⟨z, hz.1.1⟩ 99 calc 100 chart y z = f zs := hyq zs (by simpa only [zs, mem_ball] using hz.2) 101 _ = chart x z := 102 (hxr zs (by simpa only [zs, mem_ball] using hz.1.2)).symm 103 exact affineIsometryEquiv_eq_of_isOpen_of_eqOn hu hune (chart y) (chart x) heq 104 let x₀ : s := ⟨Classical.choose hsc.nonempty, Classical.choose_spec hsc.nonempty⟩ 105 have hconst (x y : s) : chart x = chart y := by 106 letI : PreconnectedSpace s := Subtype.preconnectedSpace hsc.isPreconnected 107 exact hchart.apply_eq_of_preconnectedSpace x y 108 have hagree (x : s) : chart x₀ (x : E) = f x := by 109 rw [hconst x₀ x] 110 rcases chart_spec x with ⟨r, hr, hxr⟩ 111 exact hxr x (by simpa using hr) 112 refine ⟨chart x₀, hagree, ?_⟩ 113 intro A hA 114 apply affineIsometryEquiv_eq_of_isOpen_of_eqOn hs hsc.nonempty A (chart x₀) 115 intro z hz 116 calc 117 A z = f ⟨z, hz⟩ := hA ⟨z, hz⟩ 118 _ = chart x₀ z := (hagree ⟨z, hz⟩).symm 119 120 /-- A surjective isometry between open connected subsets of real normed 121 spaces extends to a unique ambient real affine isometry equivalence. -/ 122 theorem existsUnique_affineExtension 123 {s : Set E} {t : Set F} (f : s ≃ᵢ t) 124 (hs : IsOpen s) (hsc : IsConnected s) (ht : IsOpen t) : 125 ∃! A : E ≃ᵃⁱ[ℝ] F, 126 ∀ x : s, A (x : E) = ((f x : t) : F) := by 127 have hlocal : ∀ x : s, ∃ A : E ≃ᵃⁱ[ℝ] F, ∃ r > 0, 128 ∀ y : s, dist (y : E) (x : E) < r → 129 A (y : E) = ((f y : t) : F) := by 130 intro x 131 rcases Metric.mem_nhds_iff.1 (hs.mem_nhds x.property) with 132 ⟨Rs, hRs, hsball⟩ 133 rcases Metric.mem_nhds_iff.1 (ht.mem_nhds (f x).property) with 134 ⟨Rt, hRt, htball⟩ 135 let R : ℝ := min Rs Rt 136 have hR : 0 < R := lt_min hRs hRt 137 have hsball' : ball (x : E) R ⊆ s := 138 (ball_subset_ball (min_le_left Rs Rt)).trans hsball 139 have htball' : ball ((f x : t) : F) R ⊆ t := 140 (ball_subset_ball (min_le_right Rs Rt)).trans htball 141 rcases MathlibAnnex.IsometryEquiv.exists_affineExtension_eqOn_ball 142 f x hR hsball' htball' with ⟨A, hA⟩ 143 refine ⟨A, R / 8, by positivity, ?_⟩ 144 intro y hy 145 exact hA y (by simpa only [mem_ball] using hy) 146 exact existsUnique_affineIsometryEquiv_of_local hs hsc 147 (fun x ↦ ((f x : t) : F)) hlocal 148 149 end IsometryEquiv 150 151 end 152 153 end MathlibAnnex