Exact UTF-8 source: MathlibAnnex/Analysis/Normed/Affine/IsometryExtension/OpenConnected.lean
Download exact raw UTF-8 source
1import MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Local2import Mathlib.Topology.LocallyConstant.Basic34/-!5# Extension from open connected domains67This module glues the local affine-isometry extensions into a unique ambient8affine isometry equivalence.9-/1011open Metric Set AffineIsometryEquiv1213namespace MathlibAnnex1415noncomputable section1617variable {E F : Type*}18 [NormedAddCommGroup E] [NormedSpace ℝ E]19 [NormedAddCommGroup F] [NormedSpace ℝ F]2021namespace IsometryEquiv2223private theorem affineIsometryEquiv_map_lineMap24 (A : E ≃ᵃⁱ[ℝ] F) (c x : E) (a : ℝ) :25 A (AffineMap.lineMap c x a) =26 AffineMap.lineMap (A c) (A x) a := by27 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 c33 rw [LinearMap.map_smul, A.toAffineEquiv.toAffineMap.linearMap_vsub]34 rfl3536private theorem affineIsometryEquiv_eq_of_eqOn_open37 {u : Set E} (hu : IsOpen u) (hne : u.Nonempty)38 (A B : E ≃ᵃⁱ[ℝ] F) (h : u.EqOn A B) : A = B := by39 rcases hne with ⟨c, hc⟩40 rcases Metric.mem_nhds_iff.1 (hu.mem_nhds hc) with ⟨ε, hε, hball⟩41 apply AffineIsometryEquiv.ext42 intro x43 by_cases hxc : x = c44 · subst x45 exact h hc46 let a : ℝ := ε / (2 * dist x c)47 have hd : 0 < dist x c := dist_pos.mpr hxc48 have ha : 0 < a := div_pos hε (mul_pos (by norm_num) hd)49 let y : E := AffineMap.lineMap c x a50 have hyc : dist y c = ε / 2 := by51 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_simp57 have hy : y ∈ u := by58 apply hball59 rw [mem_ball, hyc]60 linarith61 have hcAB : A c = B c := h hc62 have hyAB : A y = B y := h hy63 have hline : AffineMap.lineMap (A c) (A x) a =64 AffineMap.lineMap (B c) (B x) a := by65 rw [← affineIsometryEquiv_map_lineMap A c x a,66 ← affineIsometryEquiv_map_lineMap B c x a]67 exact hyAB68 rw [AffineMap.lineMap_apply_module', AffineMap.lineMap_apply_module', hcAB] at hline69 have hv : A x - B c = B x - B c := by70 apply smul_right_injective F ha.ne'71 exact add_right_cancel hline72 exact sub_left_injective hv7374private theorem glue_local_affine_isometry75 {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 := by79 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 := by84 rw [IsLocallyConstant.iff_eventually_eq]85 intro x86 rcases chart_spec x with ⟨r, hr, hxr⟩87 filter_upwards [ball_mem_nhds x hr] with y hy88 rcases chart_spec y with ⟨q, hq, hyq⟩89 let u : Set E := (s ∩ ball (x : E) r) ∩ ball (y : E) q90 have hu : IsOpen u := (hs.inter isOpen_ball).inter isOpen_ball91 have hyx : dist (y : E) (x : E) < r := by92 simpa only [mem_ball, Subtype.dist_eq] using hy93 have hune : u.Nonempty := by94 refine ⟨(y : E), ⟨y.property, ?_⟩, mem_ball_self hq⟩95 exact hyx96 have heq : u.EqOn (chart y) (chart x) := by97 intro z hz98 let zs : s := ⟨z, hz.1.1⟩99 calc100 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)).symm103 exact affineIsometryEquiv_eq_of_eqOn_open hu hune (chart y) (chart x) heq104 let x₀ : s := ⟨Classical.choose hsc.nonempty, Classical.choose_spec hsc.nonempty⟩105 have hconst (x y : s) : chart x = chart y := by106 letI : PreconnectedSpace s := Subtype.preconnectedSpace hsc.isPreconnected107 exact hchart.apply_eq_of_preconnectedSpace x y108 have hagree (x : s) : chart x₀ (x : E) = f x := by109 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 hA114 apply affineIsometryEquiv_eq_of_eqOn_open hs hsc.nonempty A (chart x₀)115 intro z hz116 calc117 A z = f ⟨z, hz⟩ := hA ⟨z, hz⟩118 _ = chart x₀ z := (hagree ⟨z, hz⟩).symm119120/-- A surjective isometry between open connected subsets of real normed121spaces extends to a unique ambient real affine isometry equivalence. -/122theorem existsUnique_affineExtension123 {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) := by127 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) := by130 intro x131 rcases Metric.mem_nhds_iff.1 (hs.mem_nhds x.property) with132 ⟨Rs, hRs, hsball⟩133 rcases Metric.mem_nhds_iff.1 (ht.mem_nhds (f x).property) with134 ⟨Rt, hRt, htball⟩135 let R : ℝ := min Rs Rt136 have hR : 0 < R := lt_min hRs hRt137 have hsball' : ball (x : E) R ⊆ s :=138 (ball_subset_ball (min_le_left Rs Rt)).trans hsball139 have htball' : ball ((f x : t) : F) R ⊆ t :=140 (ball_subset_ball (min_le_right Rs Rt)).trans htball141 rcases MathlibAnnex.IsometryEquiv.exists_affineExtension_eqOn_ball142 f x hR hsball' htball' with ⟨A, hA⟩143 refine ⟨A, R / 8, by positivity, ?_⟩144 intro y hy145 exact hA y (by simpa only [mem_ball] using hy)146 exact glue_local_affine_isometry hs hsc147 (fun x ↦ ((f x : t) : F)) hlocal148149end IsometryEquiv150151end152153end MathlibAnnex