Extension.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The unique real-linear extension of an onto sphere isometry

The intermediate hypotheses of the separate constructions are discharged here: positive original defect produces an actual attained defect in completed normed quotients, alignment produces actual opposite chords, and the chord theorem rules them out. The original radial extension consequently preserves distance.

theorem OAI.Tingley.no_attained_positive_defect line 27
theorem OAI.Tingley.maxDefect_eq_zero line 39
theorem OAI.Tingley.hasDefectBound_zero line 53
theorem OAI.Tingley.existsUnique_linearIsometryEquiv line 56
def OAI.Tingley.extension line 62
Source documentation
The actual unconditional extension, with the original radial function.
```
def extension (f : UnitSphere X ≃ᵢ UnitSphere Y) : X ≃ₗᵢ[ℝ] Y :=
…
```
Mentions: OAI.Tingley.UnitSphere
theorem OAI.Tingley.extension_apply line 65
theorem OAI.Tingley.extension_zero line 68
theorem OAI.Tingley.extension_unit line 71
theorem OAI.Tingley.extension_radial line 74
theorem OAI.Tingley.extension_surjective line 78
theorem OAI.Tingley.extension_unique line 81
def OAI.Tingley.sphereIsometryEquiv line 89
Source documentation
An ordinary onto sphere isometry is a genuine sphere isometry equivalence.
```
def sphereIsometryEquiv (f : UnitSphere X → UnitSphere Y)
    (hf : Isometry f) (hs : Function.Surjective f) : UnitSphere X ≃ᵢ UnitSphere Y where
…
```
Mentions: OAI.Tingley.UnitSphere

theorem OAI.Tingley.tingley_sphere_isometry line 95

Source documentation

Every onto isometry of unit spheres extends uniquely to a real-linear isometry.

theorem tingley_sphere_isometry
    (f : UnitSphere X → UnitSphere Y) (hf : Isometry f) (hs : Function.Surjective f) :
    ∃! T : X ≃ₗᵢ[ℝ] Y, ∀ x : UnitSphere X, T (x : X) = (f x : Y) := by
…

Mentions: OAI.Tingley.UnitSphere

theorem OAI.Tingley.tingley_sphere_isometry_full line 101

Source documentation

Radial formula, surjectivity, and uniqueness among all real-linear extensions.

Distinct definitions of this name: ComparatorChallenges/TingleySphereIsometry.lean:22 (different declaration text). Qualify references as OAI.Tingley.tingley_sphere_isometry_full@path.

theorem tingley_sphere_isometry_full
    (f : UnitSphere X → UnitSphere Y) (hf : Isometry f) (hs : Function.Surjective f) :
    ∃ T : X ≃ₗᵢ[ℝ] Y,
      (∀ u : UnitSphere X, T (u : X) = (f u : Y)) ∧
      T 0 = 0 ∧
      (∀ x : X, ∀ hx : x ≠ 0, T x = ‖x‖ • (f (normalize x hx) : Y)) ∧
      Function.Surjective T ∧
      (∀ L : X →ₗ[ℝ] Y, (∀ u : UnitSphere X, L (u : X) = (f u : Y)) →
        L = T.toLinearEquiv.toLinearMap) := by
…

Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.normalize