English
For any x,y ∈ P, dist(pointReflection x y, y) = 2 · dist(x, y).
Русский
Для любых x,y ∈ P, dist(pointReflection x y, y) = 2 · dist(x,y).
LaTeX
$$$\operatorname{dist}(\operatorname{pointReflection}_{\mathbb{k}}(x)(y), y) = 2 \cdot \operatorname{dist}(x,y)$$$
Lean4
/-- If an isometric self-homeomorphism of a normed vector space over `ℝ` fixes `x` and `y`,
then it fixes the midpoint of `[x, y]`. This is a lemma for a more general Mazur-Ulam theorem,
see below. -/
theorem midpoint_fixed {x y : PE} : ∀ e : PE ≃ᵢ PE, e x = x → e y = y → e (midpoint ℝ x y) = midpoint ℝ x y :=
by
set z := midpoint ℝ x y
set s := {e : PE ≃ᵢ PE | e x = x ∧ e y = y}
haveI : Nonempty s :=
⟨⟨IsometryEquiv.refl PE, rfl, rfl⟩⟩
-- On the one hand, `e` cannot send the midpoint `z` of `[x, y]` too far
have h_bdd : BddAbove (range fun e : s => dist ((e : PE ≃ᵢ PE) z) z) :=
by
refine ⟨dist x z + dist x z, forall_mem_range.2 <| Subtype.forall.2 ?_⟩
rintro e ⟨hx, _⟩
calc
dist (e z) z ≤ dist (e z) x + dist x z := dist_triangle (e z) x z
_ = dist (e x) (e z) + dist x z := by rw [hx, dist_comm]
_ = dist x z + dist x z := by
rw [e.dist_eq x z]
-- On the other hand, consider the map `f : (E ≃ᵢ E) → (E ≃ᵢ E)`
-- sending each `e` to `R ∘ e⁻¹ ∘ R ∘ e`, where `R` is the point reflection in the
-- midpoint `z` of `[x, y]`.
set R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv
set f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R
have hf_dist : ∀ e, dist (f e z) z = 2 * dist (e z) z :=
by
intro e
dsimp only [trans_apply, coe_toIsometryEquiv, f, R]
rw [dist_pointReflection_fixed, ← e.dist_eq, e.apply_symm_apply, dist_pointReflection_self_real, dist_comm]
-- Also note that `f` maps `s` to itself
have hf_maps_to : MapsTo f s s := by
rintro e ⟨hx, hy⟩
constructor <;>
simp [f, R, z, hx, hy, e.symm_apply_eq.2 hx.symm, e.symm_apply_eq.2 hy.symm]
-- Therefore, `dist (e z) z = 0` for all `e ∈ s`.
set c := ⨆ e : s, dist ((e : PE ≃ᵢ PE) z) z
have : c ≤ c / 2 := by
apply ciSup_le
rintro ⟨e, he⟩
simp only [le_div_iff₀' (zero_lt_two' ℝ), ← hf_dist]
exact le_ciSup h_bdd ⟨f e, hf_maps_to he⟩
replace : c ≤ 0 := by linarith
refine fun e hx hy => dist_le_zero.1 (le_trans ?_ this)
exact le_ciSup h_bdd ⟨e, hx, hy⟩
