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:

• IsometryEquiv.toRealLinearIsometryEquivOfMapZero : given E ≃ᵢ F sending 0 to 0, returns E ≃ₗᵢ[ℝ] F with the same toFun and invFun;
• IsometryEquiv.toRealLinearIsometryEquiv : given f : E ≃ᵢ F, returns a linear isometry equivalence g : E ≃ₗᵢ[ℝ] F with g x = f x - f 0.
• IsometryEquiv.toRealAffineIsometryEquiv : given f : PE ≃ᵢ PF, returns an affine isometry equivalence g : PE ≃ᵃⁱ[ℝ] PF whose underlying IsometryEquiv is f

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

Tags

isometry, affine map, linear map

theorem IsometryEquiv.midpoint_fixed {E : Type u_1} {PE : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MetricSpace PE] [NormedAddTorsor E PE] {x y : PE} (e : PE ≃ᵢ PE) : e x = x → e y = y → e (midpoint ℝ x y) = midpoint ℝ x 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 IsometryEquiv.map_midpoint {E : Type u_1} {PE : Type u_2} {F : Type u_3} {PF : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MetricSpace PE] [NormedAddTorsor E PE] [NormedAddCommGroup F] [NormedSpace ℝ F] [MetricSpace PF] [NormedAddTorsor F PF] (f : PE ≃ᵢ PF) (x y : PE) : f (midpoint ℝ x y) = midpoint ℝ (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 ContinuousLinearEquiv first, then a conversion to an AffineMap.

def IsometryEquiv.toRealLinearIsometryEquivOfMapZero {E : Type u_1} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E ≃ᵢ F) (h0 : f 0 = 0) : E ≃ₗᵢ[ℝ] F

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

• f.toRealLinearIsometryEquivOfMapZero h0 = { toLinearMap := ↑((AddMonoidHom.ofMapMidpoint ℝ ℝ (⇑f) h0 ⋯).toRealLinearMap ⋯), invFun := f.invFun, left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

@[simp]

theorem IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero {E : Type u_1} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E ≃ᵢ F) (h0 : f 0 = 0) : ⇑(f.toRealLinearIsometryEquivOfMapZero h0) = ⇑f

@[simp]

theorem IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero_symm {E : Type u_1} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E ≃ᵢ F) (h0 : f 0 = 0) : ⇑(f.toRealLinearIsometryEquivOfMapZero h0).symm = ⇑f.symm

def IsometryEquiv.toRealLinearIsometryEquiv {E : Type u_1} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E ≃ᵢ 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

• f.toRealLinearIsometryEquiv = (f.trans (IsometryEquiv.addRight (f 0)).symm).toRealLinearIsometryEquivOfMapZero ⋯

@[simp]

theorem IsometryEquiv.toRealLinearIsometryEquiv_apply {E : Type u_1} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E ≃ᵢ F) (x : E) : f.toRealLinearIsometryEquiv x = f x - f 0

@[simp]

theorem IsometryEquiv.toRealLinearIsometryEquiv_symm_apply {E : Type u_1} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E ≃ᵢ F) (y : F) : f.toRealLinearIsometryEquiv.symm y = f.symm (y + f 0)

def IsometryEquiv.toRealAffineIsometryEquiv {E : Type u_1} {PE : Type u_2} {F : Type u_3} {PF : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MetricSpace PE] [NormedAddTorsor E PE] [NormedAddCommGroup F] [NormedSpace ℝ F] [MetricSpace PF] [NormedAddTorsor F PF] (f : PE ≃ᵢ PF) : 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsometryEquiv.coeFn_toRealAffineIsometryEquiv {E : Type u_1} {PE : Type u_2} {F : Type u_3} {PF : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MetricSpace PE] [NormedAddTorsor E PE] [NormedAddCommGroup F] [NormedSpace ℝ F] [MetricSpace PF] [NormedAddTorsor F PF] (f : PE ≃ᵢ PF) : ⇑f.toRealAffineIsometryEquiv = ⇑f

@[simp]

theorem IsometryEquiv.coe_toRealAffineIsometryEquiv {E : Type u_1} {PE : Type u_2} {F : Type u_3} {PF : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MetricSpace PE] [NormedAddTorsor E PE] [NormedAddCommGroup F] [NormedSpace ℝ F] [MetricSpace PF] [NormedAddTorsor F PF] (f : PE ≃ᵢ PF) : f.toRealAffineIsometryEquiv.toIsometryEquiv = f