Exact UTF-8 source: MathlibAnnex/Analysis/Normed/Affine/Reflection.lean
Download exact raw UTF-8 source
1import Mathlib.Analysis.Normed.Affine.MazurUlam2import Mathlib.Topology.MetricSpace.Bounded3import Mathlib.Tactic.Linarith45/-!6# Centers of bounded reflection-invariant sets78Mathlib is the canonical provider of the Mazur--Ulam theorem. This module adds9one general center-transport result for bounded point-reflection-invariant10subsets. It does not provide another Mazur--Ulam endpoint.11-/1213open Metric Set AffineIsometryEquiv Bornology1415namespace MathlibAnnex.IsometryEquiv1617noncomputable section1819variable {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]2223private def restrictedPointReflection (s : Set P) (c : P)24 (h : MapsTo (pointReflection ℝ c) s s) : s ≃ᵢ s where25 toFun x := ⟨pointReflection ℝ c x, h x.property⟩26 invFun x := ⟨pointReflection ℝ c x, h x.property⟩27 left_inv x := by28 apply Subtype.ext29 exact pointReflection_involutive c (x : P)30 right_inv x := by31 apply Subtype.ext32 exact pointReflection_involutive c (x : P)33 isometry_toFun := Isometry.of_dist_eq fun x y => by34 change dist (pointReflection ℝ c (x : P)) (pointReflection ℝ c (y : P)) =35 dist (x : P) (y : P)36 exact (pointReflection ℝ c).isometry.dist_eq _ _3738private theorem fix_center_of_bounded_pointReflection_invariant39 {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⟩ := by42 let c₀ : s := ⟨c, hc⟩43 let R : s ≃ᵢ s := restrictedPointReflection s c hreflect44 have h_bdd : BddAbove (range fun e : s ≃ᵢ s => dist (e c₀) c₀) := by45 rcases (Metric.isBounded_iff.mp hs) with ⟨C, hC⟩46 refine ⟨C, forall_mem_range.2 ?_⟩47 intro g48 exact hC (g c₀).property c₀.property49 let T : (s ≃ᵢ s) → (s ≃ᵢ s) := fun g => ((g.trans R).trans g.symm).trans R50 have hT_dist : ∀ g : s ≃ᵢ s, dist (T g c₀) c₀ = 2 * dist (g c₀) c₀ := by51 intro g52 change dist (R (g.symm (R (g c₀)))) c₀ = 2 * dist (g c₀) c₀53 calc54 dist (R (g.symm (R (g c₀)))) c₀ = dist (g.symm (R (g c₀))) c₀ := by55 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₀).symm59 _ = dist (R (g c₀)) (g c₀) := by rw [g.apply_symm_apply]60 _ = 2 * dist (g c₀) c₀ := by61 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 := by66 apply ciSup_le67 intro g68 rw [le_div_iff₀' (zero_lt_two' ℝ), ← hT_dist]69 exact le_ciSup h_bdd (T g)70 have hC_nonpos : C ≤ 0 := by linarith71 apply dist_le_zero.mp72 exact (le_ciSup h_bdd e).trans hC_nonpos7374/-- An isometry equivalence between point-reflection-invariant subsets sends75the center of a bounded source subset to the center of the target subset. -/76theorem map_center_of_reflectionInvariant77 {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⟩ := by82 let R : t ≃ᵢ t := restrictedPointReflection t d htreflect83 let g : s ≃ᵢ s := (f.trans R).trans f.symm84 have hg := fix_center_of_bounded_pointReflection_invariant hc hs hsreflect g85 have hRf : R (f ⟨c, hc⟩) = f ⟨c, hc⟩ := by86 simpa [g] using congrArg f hg87 apply Subtype.ext88 have hfixed : pointReflection ℝ d ((f ⟨c, hc⟩ : t) : Q) =89 ((f ⟨c, hc⟩ : t) : Q) := by90 exact congrArg Subtype.val hRf91 exact pointReflection_fixed_iff.mp hfixed9293end9495end MathlibAnnex.IsometryEquiv