# mathlibdocumentation

analysis.normed_space.mazur_ulam

# Mazur-Ulam Theorem #

Mazur-Ulam theorem states that an isometric bijection between two normed affine spaces over ℝ is affine. We formalize it in three definitions:

• isometric.to_real_linear_isometry_equiv_of_map_zero : given E ≃ᵢ F sending 0 to 0, returns E ≃ₗᵢ[ℝ] F with the same to_fun and inv_fun;
• isometric.to_real_linear_isometry_equiv : given f : E ≃ᵢ F, returns a linear isometry equivalence g : E ≃ₗᵢ[ℝ] F with g x = f x - f 0.
• isometric.to_real_affine_isometry_equiv : given f : PE ≃ᵢ PF, returns an affine isometry equivalence g : PE ≃ᵃⁱ[ℝ] PF whose underlying isometric is f

The formalization is based on Jussi Väisälä, A Proof of the Mazur-Ulam Theorem.

## Tags #

isometry, affine map, linear map

theorem isometric.midpoint_fixed {E : Type u_1} {PE : Type u_2} [normed_group E] [ E] [metric_space PE] [ PE] {x y : PE} (e : PE ≃ᵢ PE) :
e x = xe y = ye x y) = y

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 isometric.map_midpoint {E : Type u_1} {PE : Type u_2} [normed_group E] [ E] [metric_space PE] [ PE] {F : Type u_3} {PF : Type u_4} [normed_group F] [ F] [metric_space PF] [ PF] (f : PE ≃ᵢ PF) (x y : PE) :
f x y) = (f x) (f y)

A bijective isometry sends midpoints to midpoints.

Since f : PE ≃ᵢ PF sends midpoints to midpoints, it is an affine map. We define a conversion to a continuous_linear_equiv first, then a conversion to an affine_map.

def isometric.to_real_linear_isometry_equiv_of_map_zero {E : Type u_1} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E ≃ᵢ F) (h0 : f 0 = 0) :

Mazur-Ulam Theorem: if f is an isometric bijection between two normed vector spaces over ℝ and f 0 = 0, then f is a linear isometry equivalence.

Equations
@[simp]
theorem isometric.coe_to_real_linear_equiv_of_map_zero {E : Type u_1} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E ≃ᵢ F) (h0 : f 0 = 0) :
@[simp]
theorem isometric.coe_to_real_linear_equiv_of_map_zero_symm {E : Type u_1} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E ≃ᵢ F) (h0 : f 0 = 0) :
= (f.symm)
def isometric.to_real_linear_isometry_equiv {E : Type u_1} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E ≃ᵢ F) :

Mazur-Ulam Theorem: if f is an isometric bijection between two normed vector spaces over ℝ, then x ↦ f x - f 0 is a linear isometry equivalence.

Equations
@[simp]
theorem isometric.to_real_linear_equiv_apply {E : Type u_1} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E ≃ᵢ F) (x : E) :
= f x - f 0
@[simp]
theorem isometric.to_real_linear_isometry_equiv_symm_apply {E : Type u_1} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E ≃ᵢ F) (y : F) :
= (f.symm) (y + f 0)
def isometric.to_real_affine_isometry_equiv {E : Type u_1} {PE : Type u_2} [normed_group E] [ E] [metric_space PE] [ PE] {F : Type u_3} {PF : Type u_4} [normed_group F] [ F] [metric_space PF] [ PF] (f : PE ≃ᵢ PF) :

Mazur-Ulam Theorem: if f is an isometric bijection between two normed add-torsors over normed vector spaces over ℝ, then f is an affine isometry equivalence.

Equations
@[simp]
theorem isometric.coe_fn_to_real_affine_isometry_equiv {E : Type u_1} {PE : Type u_2} [normed_group E] [ E] [metric_space PE] [ PE] {F : Type u_3} {PF : Type u_4} [normed_group F] [ F] [metric_space PF] [ PF] (f : PE ≃ᵢ PF) :
@[simp]
theorem isometric.coe_to_real_affine_isometry_equiv {E : Type u_1} {PE : Type u_2} [normed_group E] [ E] [metric_space PE] [ PE] {F : Type u_3} {PF : Type u_4} [normed_group F] [ F] [metric_space PF] [ PF] (f : PE ≃ᵢ PF) :