UltraSphere.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

The actual sphere map on the ultranorm quotient

Unit representatives exist even when the original coordinates vanish. The map and its inverse are induced coordinatewise, and every fixed real radius has the exact ultralimit defect formula.

def OAI.Tingley.unitSequence line 25
Source documentation
Every sequence of unit vectors is uniformly bounded.
```
def unitSequence (U : Ultrafilter ℕ) (s : ℕ → UnitSphere X) : UltraSequence U X :=
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.UltraSequence
theorem OAI.Tingley.unitSequence_apply line 28
def OAI.Tingley.unitClass line 32
Source documentation
The actual class of a sequence of unit vectors.
```
def unitClass (U : Ultrafilter ℕ) (s : ℕ → UnitSphere X) : UnitSphere (UltraQuotient U X) :=
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.UltraQuotient
theorem OAI.Tingley.unitClass_val line 36
theorem OAI.Tingley.norm_sub_unitClass line 39
theorem OAI.Tingley.unitClass_eq_iff line 45
theorem OAI.Tingley.unitClass_surjective line 50
def OAI.Tingley.unitRep line 73
Source documentation
Choice selects actual unit representatives after surjectivity is proved.
```
def unitRep [Nontrivial X] (U : Ultrafilter ℕ) (z : UnitSphere (UltraQuotient U X)) :
    ℕ → UnitSphere X :=
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.UltraQuotient
theorem OAI.Tingley.unitRep_spec line 77
theorem OAI.Tingley.unitClass_map_eq line 81
def OAI.Tingley.ultraSphereMap line 87
theorem OAI.Tingley.ultraSphereMap_unitClass line 91
theorem OAI.Tingley.ultraSphereMap_isometry line 96

def OAI.Tingley.ultraSphereEquiv line 108

Source documentation

Surjectivity comes from the actual coordinatewise inverse, not from isometry alone.

def ultraSphereEquiv [Nontrivial X] [Nontrivial Y] (U : Ultrafilter ℕ)
    (f : UnitSphere X ≃ᵢ UnitSphere Y) :
    UnitSphere (UltraQuotient U X) ≃ᵢ UnitSphere (UltraQuotient U Y) where
…

Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.UltraQuotient

theorem OAI.Tingley.ultraSphereEquiv_unitClass line 121
theorem OAI.Tingley.ultraSphereEquiv_symm line 126

theorem OAI.Tingley.norm_sub_smul_unitClass line 133

Source documentation

The radius-scaled norm is inherited from the linear quotient projection.

theorem norm_sub_smul_unitClass (U : Ultrafilter ℕ) (q : ℝ) (s t : ℕ → UnitSphere X) :
    ‖(unitClass U s : UltraQuotient U X) - q • (unitClass U t : UltraQuotient U X)‖ =
      realULim U (fun n => ‖(s n : X) - q • (t n : X)‖) := by
…

Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.unitClass, OAI.Tingley.UltraQuotient, OAI.Tingley.realULim

theorem OAI.Tingley.unitPairNorm_bounded line 140
theorem OAI.Tingley.signedDefect_sequence_bounded line 148

theorem OAI.Tingley.signedDefect_ultraSphereEquiv line 155

Source documentation

Exact defect formula at every fixed real radius.

theorem signedDefect_ultraSphereEquiv [Nontrivial X] [Nontrivial Y]
    (U : Ultrafilter ℕ) (f : UnitSphere X ≃ᵢ UnitSphere Y) (q : ℝ)
    (s t : ℕ → UnitSphere X) :
    signedDefect (ultraSphereEquiv U f) q (unitClass U s) (unitClass U t) =
      realULim U (fun n => signedDefect f q (s n) (t n)) := by
…

Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.signedDefect, OAI.Tingley.ultraSphereEquiv, OAI.Tingley.unitClass, OAI.Tingley.realULim

theorem OAI.Tingley.HasDefectBound.ultraSphereEquiv line 166

Source documentation

One ultrafilter transfers the bound for each arbitrarily chosen real radius.

theorem HasDefectBound.ultraSphereEquiv [Nontrivial X] [Nontrivial Y]
    {f : UnitSphere X ≃ᵢ UnitSphere Y} {M : ℝ} (h : HasDefectBound f M)
    (U : Ultrafilter ℕ) : HasDefectBound (ultraSphereEquiv U f) M := by
…

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