mathlib3 documentation

analysis.normed_space.mazur_ulam

Mazur-Ulam Theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Tags #

isometry, affine map, linear map

theorem isometry_equiv.midpoint_fixed {E : Type u_1} {PE : Type u_2} [normed_add_comm_group E] [normed_space E] [metric_space PE] [normed_add_torsor 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 isometry_equiv.map_midpoint {E : Type u_1} {PE : Type u_2} {F : Type u_3} {PF : Type u_4} [normed_add_comm_group E] [normed_space E] [metric_space PE] [normed_add_torsor E PE] [normed_add_comm_group F] [normed_space F] [metric_space PF] [normed_add_torsor 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 continuous_linear_equiv first, then a conversion to an affine_map.

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

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

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