DefectAttainment.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Positive maximal defect is attained on actual completed ultranorm spaces

The final spaces, sphere isometry, inverse, and bound are all constructed. The orientation disjunction keeps the same original maximal absolute defect.

def OAI.Tingley.completedUltraSphereEquiv line 25
Source documentation
The actual coordinatewise sphere equivalence followed by ambient completion.
```
def completedUltraSphereEquiv (U : Ultrafilter ℕ) (f : UnitSphere X ≃ᵢ UnitSphere Y) :
    UnitSphere (UltraCompletion U X) ≃ᵢ UnitSphere (UltraCompletion U Y) :=
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.UltraCompletion
theorem OAI.Tingley.completedUltraSphereEquiv_symm line 29

theorem OAI.Tingley.signedDefect_completedUltraSphereEquiv line 35

Source documentation

Exact fixed-radius formula on the canonical embedded unit classes.

theorem signedDefect_completedUltraSphereEquiv (U : Ultrafilter ℕ)
    (f : UnitSphere X ≃ᵢ UnitSphere Y) (q : ℝ) (s t : ℕ → UnitSphere X) :
    signedDefect (completedUltraSphereEquiv U f) q
      (sphereCoe (UltraQuotient U X) (unitClass U s))
      (sphereCoe (UltraQuotient U X) (unitClass U t)) =
        realULim U (fun n => signedDefect f q (s n) (t n)) := by
…

Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.signedDefect, OAI.Tingley.completedUltraSphereEquiv, OAI.Tingley.sphereCoe, OAI.Tingley.UltraQuotient, OAI.Tingley.unitClass, OAI.Tingley.realULim

theorem OAI.Tingley.HasDefectBound.completedUltraSphereEquiv line 44
theorem OAI.Tingley.positive_maxDefect_attained_or_inverse line 51
Source documentation
Positive original maximal absolute defect is attained, with the same global bound, in one orientation on explicitly constructed nonzero real Banach spaces.
```
theorem positive_maxDefect_attained_or_inverse
    (f : UnitSphere X ≃ᵢ UnitSphere Y) (hM : 0 < maxDefect f) :
    let F := completedUltraSphereEquiv freeUltrafilter f
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.maxDefect, OAI.Tingley.completedUltraSphereEquiv, OAI.Tingley.freeUltrafilter