MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.IsometryEquiv.map_center_of_mapsTo_pointReflection

Raw UTF-8 source

theorem map_center_of_mapsTo_pointReflection
    {s : Set P} {t : Set Q} {c : P} {d : Q} (f : s ≃ᵢ t)
    (hc : c ∈ s) (hd : d ∈ t) (hs : IsBounded s)
    (hsreflect : MapsTo (pointReflection ℝ c) s s)
    (htreflect : MapsTo (pointReflection ℝ d) t t) :
    f ⟨c, hc⟩ = ⟨d, hd⟩

1 import Mathlib.Analysis.Normed.Affine.MazurUlam
2 import Mathlib.Topology.MetricSpace.Bounded
3 import Mathlib.Tactic.Linarith
4 
5 /-!
6 # Centers of bounded reflection-invariant sets
7 
8 Mathlib is the canonical provider of the Mazur--Ulam theorem. This module adds
9 one general center-transport result for bounded point-reflection-invariant
10 subsets. It does not provide another Mazur--Ulam endpoint.
11 -/
12 
13 open Metric Set AffineIsometryEquiv Bornology
14 
15 namespace MathlibAnnex.IsometryEquiv
16 
17 noncomputable section
18 
19 variable {V P W Q : Type*}
20   [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]
21   [NormedAddCommGroup W] [NormedSpace ℝ W] [MetricSpace Q] [NormedAddTorsor W Q]
22 
23 private def restrictedPointReflection (s : Set P) (c : P)
24     (h : MapsTo (pointReflection ℝ c) s s) : s ≃ᵢ s where
25   toFun x := ⟨pointReflection ℝ c x, h x.property⟩
26   invFun x := ⟨pointReflection ℝ c x, h x.property⟩
27   left_inv x := by
28     apply Subtype.ext
29     exact pointReflection_involutive c (x : P)
30   right_inv x := by
31     apply Subtype.ext
32     exact pointReflection_involutive c (x : P)
33   isometry_toFun := Isometry.of_dist_eq fun x y => by
34     change dist (pointReflection ℝ c (x : P)) (pointReflection ℝ c (y : P)) =
35       dist (x : P) (y : P)
36     exact (pointReflection ℝ c).isometry.dist_eq _ _
37 
38 private theorem apply_center_eq_of_isBounded_of_mapsTo_pointReflection
39     {s : Set P} {c : P} (hc : c ∈ s) (hs : IsBounded s)
40     (hreflect : MapsTo (pointReflection ℝ c) s s) (e : s ≃ᵢ s) :
41     e ⟨c, hc⟩ = ⟨c, hc⟩ := by
42   let c₀ : s := ⟨c, hc⟩
43   let R : s ≃ᵢ s := restrictedPointReflection s c hreflect
44   have h_bdd : BddAbove (range fun e : s ≃ᵢ s => dist (e c₀) c₀) := by
45     rcases (Metric.isBounded_iff.mp hs) with ⟨C, hC⟩
46     refine ⟨C, forall_mem_range.2 ?_⟩
47     intro g
48     exact hC (g c₀).property c₀.property
49   let T : (s ≃ᵢ s) → (s ≃ᵢ s) := fun g => ((g.trans R).trans g.symm).trans R
50   have hT_dist : ∀ g : s ≃ᵢ s, dist (T g c₀) c₀ = 2 * dist (g c₀) c₀ := by
51     intro g
52     change dist (R (g.symm (R (g c₀)))) c₀ = 2 * dist (g c₀) c₀
53     calc
54       dist (R (g.symm (R (g c₀)))) c₀ = dist (g.symm (R (g c₀))) c₀ := by
55         rw [Subtype.dist_eq, Subtype.dist_eq]
56         exact dist_pointReflection_fixed c (g.symm (R (g c₀)) : P)
57       _ = dist (g (g.symm (R (g c₀)))) (g c₀) :=
58         (g.dist_eq (g.symm (R (g c₀))) c₀).symm
59       _ = dist (R (g c₀)) (g c₀) := by rw [g.apply_symm_apply]
60       _ = 2 * dist (g c₀) c₀ := by
61         dsimp [R, restrictedPointReflection]
62         rw [Subtype.dist_eq, Subtype.dist_eq]
63         simpa [dist_comm] using dist_pointReflection_self_real c (g c₀ : P)
64   let C := ⨆ g : s ≃ᵢ s, dist (g c₀) c₀
65   have hhalve : C ≤ C / 2 := by
66     apply ciSup_le
67     intro g
68     rw [le_div_iff₀' (zero_lt_two' ℝ), ← hT_dist]
69     exact le_ciSup h_bdd (T g)
70   have hC_nonpos : C ≤ 0 := by linarith
71   apply dist_le_zero.mp
72   exact (le_ciSup h_bdd e).trans hC_nonpos
73 
74 /-- An isometry equivalence between point-reflection-invariant subsets sends
75 the center of a bounded source subset to the center of the target subset. -/
76 theorem map_center_of_mapsTo_pointReflection
77     {s : Set P} {t : Set Q} {c : P} {d : Q} (f : s ≃ᵢ t)
78     (hc : c ∈ s) (hd : d ∈ t) (hs : IsBounded s)
79     (hsreflect : MapsTo (pointReflection ℝ c) s s)
80     (htreflect : MapsTo (pointReflection ℝ d) t t) :
81     f ⟨c, hc⟩ = ⟨d, hd⟩ := by
82   let R : t ≃ᵢ t := restrictedPointReflection t d htreflect
83   let g : s ≃ᵢ s := (f.trans R).trans f.symm
84   have hg := apply_center_eq_of_isBounded_of_mapsTo_pointReflection hc hs hsreflect g
85   have hRf : R (f ⟨c, hc⟩) = f ⟨c, hc⟩ := by
86     simpa [g] using congrArg f hg
87   apply Subtype.ext
88   have hfixed : pointReflection ℝ d ((f ⟨c, hc⟩ : t) : Q) =
89       ((f ⟨c, hc⟩ : t) : Q) := by
90     exact congrArg Subtype.val hRf
91   exact pointReflection_fixed_iff.mp hfixed
92 
93 end
94 
95 end MathlibAnnex.IsometryEquiv