MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_ball

Raw UTF-8 source

theorem existsUnique_affineExtension_ball
    {c : E} {d : F} {r R : ℝ} (f : ball c r ≃ᵢ ball d R)
    (hr : 0 < r) (hR : 0 < R) :
    ∃! A : E ≃ᵃⁱ[ℝ] F,
      ∀ x : ball c r, A (x : E) = ((f x : ball d R) : F)

1 import MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Convex
2 import Mathlib.Analysis.Normed.Module.Connected
3 import Mathlib.Analysis.Normed.Module.RCLike.Real
4 
5 /-!
6 # Ball extension corollaries
7 
8 The closed-ball theorem first transports the center using the bounded
9 point-reflection theorem, then applies the convex ambient-interior corollary.
10 -/
11 
12 open Metric Set AffineIsometryEquiv Bornology
13 
14 namespace MathlibAnnex
15 
16 noncomputable section
17 
18 variable {E F : Type*}
19   [NormedAddCommGroup E] [NormedSpace ℝ E]
20   [NormedAddCommGroup F] [NormedSpace ℝ F]
21 
22 namespace IsometryEquiv
23 
24 /-- A surjective isometry between positive-radius open balls extends to a
25 unique ambient real affine isometry equivalence. -/
26 theorem existsUnique_affineExtension_ball
27     {c : E} {d : F} {r R : ℝ} (f : ball c r ≃ᵢ ball d R)
28     (hr : 0 < r) (hR : 0 < R) :
29     ∃! A : E ≃ᵃⁱ[ℝ] F,
30       ∀ x : ball c r, A (x : E) = ((f x : ball d R) : F) := by
31   have _htc : IsConnected (ball d R) := isConnected_ball hR
32   exact MathlibAnnex.IsometryEquiv.existsUnique_affineExtension
33     f isOpen_ball (isConnected_ball hr) isOpen_ball
34 
35 private theorem mapsTo_pointReflection_closedBall (c : E) (r : ℝ) :
36     MapsTo (pointReflection ℝ c) (closedBall c r) (closedBall c r) := by
37   intro x hx
38   rw [mem_closedBall, dist_pointReflection_fixed]
39   exact hx
40 
41 /-- A surjective isometry between closed balls of the same positive radius
42 extends to a unique ambient real affine isometry equivalence. -/
43 theorem existsUnique_affineExtension_closedBall
44     {c : E} {d : F} {r : ℝ} (f : closedBall c r ≃ᵢ closedBall d r)
45     (hr : 0 < r) :
46     ∃! A : E ≃ᵃⁱ[ℝ] F,
47       ∀ x : closedBall c r,
48         A (x : E) = ((f x : closedBall d r) : F) := by
49   let cc : closedBall c r := ⟨c, mem_closedBall_self hr.le⟩
50   let dd : closedBall d r := ⟨d, mem_closedBall_self hr.le⟩
51   have hcenter : f cc = dd :=
52     MathlibAnnex.IsometryEquiv.map_center_of_mapsTo_pointReflection
53       f cc.property dd.property isBounded_closedBall
54       (mapsTo_pointReflection_closedBall c r)
55       (mapsTo_pointReflection_closedBall d r)
56   have hcenter_val : ((f cc : closedBall d r) : F) = d :=
57     congrArg Subtype.val hcenter
58   have hfi : ∀ x : closedBall c r,
59       (x : E) ∈ interior (closedBall c r) ↔
60         ((f x : closedBall d r) : F) ∈ interior (closedBall d r) := by
61     intro x
62     rw [interior_closedBall c hr.ne', interior_closedBall d hr.ne',
63       mem_ball, mem_ball]
64     have hdist : dist ((f x : closedBall d r) : F) d = dist (x : E) c := by
65       calc
66         dist ((f x : closedBall d r) : F) d =
67             dist ((f x : closedBall d r) : F)
68               ((f cc : closedBall d r) : F) := by rw [hcenter_val]
69         _ = dist (f x) (f cc) := rfl
70         _ = dist x cc := f.dist_eq x cc
71         _ = dist (x : E) c := rfl
72     rw [hdist]
73   have hsint : (interior (closedBall c r)).Nonempty := by
74     rw [interior_closedBall c hr.ne']
75     exact nonempty_ball.mpr hr
76   exact
77     MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_of_convex
78       f (convex_closedBall c r) hsint hfi
79 
80 end IsometryEquiv
81 
82 end
83 
84 end MathlibAnnex