RadialExtension.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

The radial extension of a sphere isometry with zero defect

The extension is defined on actual vectors, including zero. A zero cross-radius bound gives its all-pairs isometry; sphere surjectivity gives its surjectivity. Mazur–Ulam then supplies real linearity. Uniqueness is proved against arbitrary real-linear extensions, without assuming they are continuous or surjective.

def OAI.Tingley.radialExtension line 27
Source documentation
The actual radial extension, with a separate zero branch.
```
def radialExtension (f : UnitSphere X ≃ᵢ UnitSphere Y) (x : X) : Y := by
…
```
Mentions: OAI.Tingley.UnitSphere
theorem OAI.Tingley.radialExtension_zero line 31
theorem OAI.Tingley.radialExtension_of_ne_zero line 35
theorem OAI.Tingley.radialExtension_norm line 40
theorem OAI.Tingley.radialExtension_smul_unit line 49
Source documentation
Every nonnegative radial representation has the expected image.
```
theorem radialExtension_smul_unit (f : UnitSphere X ≃ᵢ UnitSphere Y)
    (r : ℝ) (hr : 0 ≤ r) (u : UnitSphere X) :
    radialExtension f (r • (u : X)) = r • (f u : Y) := by
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.radialExtension
theorem OAI.Tingley.radialExtension_unit line 67

theorem OAI.Tingley.crossRadius_eq_of_zero_defect line 72

Source documentation

The zero bound gives exact preservation at every radius in the closed unit interval.

theorem crossRadius_eq_of_zero_defect (f : UnitSphere X ≃ᵢ UnitSphere Y)
    (h0 : HasDefectBound f 0) (q : ℝ) (hq : q ∈ Set.Icc (0 : ℝ) 1)
    (u v : UnitSphere X) :
    ‖(f u : Y) - q • (f v : Y)‖ = ‖(u : X) - q • (v : X)‖ := by
…

Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.HasDefectBound

theorem OAI.Tingley.scaled_norm_sub_eq line 79

Source documentation

Factor by the larger positive radius; the smaller radius may be zero.

theorem scaled_norm_sub_eq (f : UnitSphere X ≃ᵢ UnitSphere Y)
    (h0 : HasDefectBound f 0) (u v : UnitSphere X) (a b : ℝ)
    (ha : 0 < a) (hb : 0 ≤ b) (hba : b ≤ a) :
    ‖a • (f u : Y) - b • (f v : Y)‖ = ‖a • (u : X) - b • (v : X)‖ := by
…

Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.HasDefectBound

theorem OAI.Tingley.radialExtension_norm_sub line 101
Source documentation
Every pair is covered, including zero vectors and either order of radii.
```
theorem radialExtension_norm_sub (f : UnitSphere X ≃ᵢ UnitSphere Y)
    (h0 : HasDefectBound f 0) (x y : X) :
    ‖radialExtension f x - radialExtension f y‖ = ‖x - y‖ := by
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.HasDefectBound, OAI.Tingley.radialExtension
theorem OAI.Tingley.radialExtension_isometry line 125
theorem OAI.Tingley.radialExtension_surjective line 132
Source documentation
Surjectivity follows directly from the actual inverse on unit spheres.
```
theorem radialExtension_surjective (f : UnitSphere X ≃ᵢ UnitSphere Y) :
    Function.Surjective (radialExtension f) := by
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.radialExtension
def OAI.Tingley.radialIsometryEquiv line 143
Source documentation
The metric equivalence is built only after isometry and surjectivity are proved.
```
def radialIsometryEquiv (f : UnitSphere X ≃ᵢ UnitSphere Y)
    (h0 : HasDefectBound f 0) : X ≃ᵢ Y where
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.HasDefectBound
theorem OAI.Tingley.coe_radialIsometryEquiv line 149
theorem OAI.Tingley.radialIsometryEquiv_apply line 152
def OAI.Tingley.radialLinearIsometryEquiv line 157
Source documentation
Mazur–Ulam applied to the derived whole-space isometry fixing zero.
```
def radialLinearIsometryEquiv (f : UnitSphere X ≃ᵢ UnitSphere Y)
    (h0 : HasDefectBound f 0) : X ≃ₗᵢ[ℝ] Y :=
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.HasDefectBound
theorem OAI.Tingley.coe_radialLinearIsometryEquiv line 162
theorem OAI.Tingley.radialLinearIsometryEquiv_apply line 166
theorem OAI.Tingley.radialLinearIsometryEquiv_unit line 170
theorem OAI.Tingley.linear_extension_eq_radial line 176
Source documentation
Any real-linear extension has the radial formula, without additional hypotheses on it.
```
theorem linear_extension_eq_radial (f : UnitSphere X ≃ᵢ UnitSphere Y)
    (L : X →ₗ[ℝ] Y) (hL : ∀ u : UnitSphere X, L (u : X) = (f u : Y)) (x : X) :
    L x = radialExtension f x := by
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.radialExtension
theorem OAI.Tingley.linear_extension_unique line 189
theorem OAI.Tingley.existsUnique_linearIsometryEquiv_of_zero_defect line 199
Source documentation
The conditional extension endpoint; the main theorem supplies the proved zero bound.
```
theorem existsUnique_linearIsometryEquiv_of_zero_defect
    (f : UnitSphere X ≃ᵢ UnitSphere Y) (h0 : HasDefectBound f 0) :
    ∃! L : X ≃ₗᵢ[ℝ] Y, ∀ u : UnitSphere X, L (u : X) = (f u : Y) := by
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.HasDefectBound