SphereCompletion.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Unit spheres and completion

The unit sphere of a normed space is dense in the unit sphere of its ambient completion. This identifies its metric completion with that completed sphere. An actual sphere isometry and its inverse therefore extend to the completed spheres, with exact preservation of the ambient fixed-radius defect.

No completeness of the original spaces, compactness, or separability is used.

instance OAI.Tingley.UnitSphere.instCompleteSpace line 30
Source documentation
A unit sphere is complete when its ambient normed space is complete.
```
instance UnitSphere.instCompleteSpace [CompleteSpace E] : CompleteSpace (UnitSphere E) :=
…
```
Mentions: OAI.Tingley.UnitSphere
def OAI.Tingley.sphereCoe line 34
Source documentation
The canonical ambient completion embedding restricted to the unit sphere.
```
def sphereCoe (E : Type u) [NormedAddCommGroup E] :
    UnitSphere E → UnitSphere (Completion E) := fun x =>
…
```
Mentions: OAI.Tingley.UnitSphere
theorem OAI.Tingley.sphereCoe_val line 39
theorem OAI.Tingley.sphereCoe_isometry line 42
theorem OAI.Tingley.norm_normalize_sub line 50
theorem OAI.Tingley.sphereCoe_denseRange line 60
Source documentation
Normalizing close old vectors proves density in the completed unit sphere.
```
theorem sphereCoe_denseRange (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] :
    DenseRange (sphereCoe E) := by
…
```
Mentions: OAI.Tingley.sphereCoe
def OAI.Tingley.sphereCompletionMap line 90
theorem OAI.Tingley.sphereCompletionMap_isometry line 94
theorem OAI.Tingley.sphereCompletionMap_coe line 99
theorem OAI.Tingley.sphereCompletionMap_surjective line 103
def OAI.Tingley.sphereCompletionEquiv line 112
Source documentation
The metric completion of the old sphere is the sphere of the ambient completion.
```
def sphereCompletionEquiv (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] :
    Completion (UnitSphere E) ≃ᵢ UnitSphere (Completion E) :=
…
```
Mentions: OAI.Tingley.UnitSphere
theorem OAI.Tingley.sphereCompletionEquiv_coe line 118
theorem OAI.Tingley.sphereCompletionEquiv_symm_coe line 122
def OAI.Tingley.sphereIsometryCompletion line 128
def OAI.Tingley.completedSphereEquiv line 145
Source documentation
Extend the actual sphere isometry and its inverse through the sphere completions.
```
def completedSphereEquiv (f : UnitSphere E ≃ᵢ UnitSphere F) :
    UnitSphere (Completion E) ≃ᵢ UnitSphere (Completion F) :=
…
```
Mentions: OAI.Tingley.UnitSphere
theorem OAI.Tingley.completedSphereEquiv_coe line 150
theorem OAI.Tingley.completedSphereEquiv_symm line 158
theorem OAI.Tingley.norm_completion_sub_smul line 165
Source documentation
The canonical ambient embedding preserves all real scalar difference norms.
```
theorem norm_completion_sub_smul (x y : E) (q : ℝ) :
    ‖(x : Completion E) - q • (y : Completion E)‖ = ‖x - q • y‖ := by
…
```
theorem OAI.Tingley.signedDefect_completedSphereEquiv_coe line 170
Source documentation
The defect on embedded old points is preserved for every real scalar.
```
@[simp] theorem signedDefect_completedSphereEquiv_coe
    (f : UnitSphere E ≃ᵢ UnitSphere F) (q : ℝ) (x y : UnitSphere E) :
    signedDefect (completedSphereEquiv f) q (sphereCoe E x) (sphereCoe E y) =
      signedDefect f q x y := by
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.signedDefect, OAI.Tingley.completedSphereEquiv, OAI.Tingley.sphereCoe
theorem OAI.Tingley.continuous_signedDefect_pair line 179
Source documentation
The fixed-radius signed defect is continuous on pairs of unit points.
```
theorem continuous_signedDefect_pair (f : UnitSphere E ≃ᵢ UnitSphere F) (q : ℝ) :
    Continuous (fun p : UnitSphere E × UnitSphere E => signedDefect f q p.1 p.2) := by
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.signedDefect
theorem OAI.Tingley.HasDefectBound.completedSphereEquiv line 192
Source documentation
Every fixed-radius bound passes to all pairs in the completed spheres.
```
theorem HasDefectBound.completedSphereEquiv {f : UnitSphere E ≃ᵢ UnitSphere F} {M : ℝ}
    (h : HasDefectBound f M) : HasDefectBound (completedSphereEquiv f) M := by
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.HasDefectBound
theorem OAI.Tingley.attainedDefect_completedSphereEquiv line 205
Source documentation
An attained signed defect remains attained at the same embedded points and scalar.
```
theorem attainedDefect_completedSphereEquiv (f : UnitSphere E ≃ᵢ UnitSphere F)
    {q M : ℝ} {x y : UnitSphere E} (h : signedDefect f q x y = M) :
    signedDefect (completedSphereEquiv f) q (sphereCoe E x) (sphereCoe E y) = M := by
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.signedDefect, OAI.Tingley.completedSphereEquiv, OAI.Tingley.sphereCoe