Documentation

Mathlib.Analysis.Normed.Affine.MazurUlam

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:

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

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 : PE} {y : PE} (e : PE ≃ᵢ PE) :
e x = xe y = ye (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 : PE) (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.

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' := }
Instances For
    @[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

    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
    Instances For
      @[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)

      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.
      Instances For
        @[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