Mazur-Ulam Theorem
Mazur-Ulam theorem states that an isometric bijection between two normed spaces over ℝ is affine.
We formalize it in two definitions:
isometric.to_real_linear_equiv_of_map_zero: givenE ≃ᵢ Fsending0to0, returnsE ≃L[ℝ] Fwith the sameto_funandinv_fun;isometric.to_real_linear_equiv: givenf : E ≃ᵢ F, returnsg : E ≃L[ℝ] Fwithg x = f x - f 0.isometric.to_affine_map: givenPE ≃ᵢ PF, returnsg : affine_map ℝ E PE F PFwith the sameto_fun.
The formalization is based on [Jussi Väisälä, A Proof of the Mazur-Ulam Theorem][Vaisala_2003].
TODO
Once we have affine equivalences, upgrade isometric.to_affine_map to isometric.to_affine_equiv.
Tags
isometry, affine map, linear map
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.
A bijective isometry sends midpoints to midpoints.
Since f : E ≃ᵢ F 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 equivalence.
Equations
- f.to_real_linear_equiv_of_map_zero h0 = {to_linear_equiv := {to_fun := ((add_monoid_hom.of_map_midpoint ℝ ℝ ⇑f h0 _).to_real_linear_map _).to_linear_map.to_fun, map_add' := _, map_smul' := _, inv_fun := f.to_homeomorph.to_equiv.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
Mazur-Ulam Theorem: if f is an isometric bijection between two normed vector spaces
over ℝ, then x ↦ f x - f 0 is a linear equivalence.
Equations
- f.to_real_linear_equiv = (f.trans (isometric.add_right (⇑f 0)).symm).to_real_linear_equiv_of_map_zero _
Convert an isometric equivalence between two affine spaces to an affine_map.
Equations
- f.to_affine_map = affine_map.mk' ⇑f ↑(((isometric.vadd_const (classical.choice isometric.to_affine_map._proof_1)).trans (f.trans (isometric.vadd_const (⇑f (classical.choice isometric.to_affine_map._proof_1))).symm)).to_real_linear_equiv) (classical.choice isometric.to_affine_map._proof_1) _