ReturnMap.lean`

60 declarations, 0 contain sorry, 0 declared as axioms

The actual radial return map

For fixed f, y and 0 < t < 1, the two interior centers are t • y and t • f y. The map follows the two radial contacts. The opposite direction is literal vector negation, with no antipodality assumption on f. The ambient extensions are continuous on the unit sphere; no continuity away from that sphere is asserted.

def OAI.Tingley.sphereNeg line 28
Source documentation
Literal negation of a unit vector.
```
def sphereNeg (v : UnitSphere X) : UnitSphere X :=
…
```
Mentions: OAI.Tingley.UnitSphere
theorem OAI.Tingley.sphereNeg_coe line 32
theorem OAI.Tingley.continuous_sphereNeg line 36
theorem OAI.Tingley.norm_smul_unitSphere line 39
theorem OAI.Tingley.returnCenter_lt_one line 43

theorem OAI.Tingley.norm_unit_sub_center_bounds line 49

Source documentation

Distances from any unit point to either interior center have uniform bounds.

theorem norm_unit_sub_center_bounds (x y : UnitSphere X) (t : ℝ) (ht : 0 ≤ t) :
    1 - t ≤ ‖(x : X) - t • (y : X)‖ ∧
      ‖(x : X) - t • (y : X)‖ ≤ 1 + t := by
…

Mentions: OAI.Tingley.UnitSphere

theorem OAI.Tingley.unit_sub_center_ne_zero line 58
theorem OAI.Tingley.center_sub_unit_ne_zero line 65
def OAI.Tingley.pRadius line 71
Source documentation
The first radial radius. The isometry is an explicit common parameter even though this first contact only uses the domain center.
```
def pRadius (_f : UnitSphere X ≃ᵢ UnitSphere Y) (y : UnitSphere X)
    (t : ℝ) (ht : 0 < t ∧ t < 1) (v : UnitSphere X) : ℝ :=
…
```
Mentions: OAI.Tingley.UnitSphere
def OAI.Tingley.xPoint line 79
Source documentation
The first contact point t y + p v.
```
def xPoint (v : UnitSphere X) : UnitSphere X :=
…
```
Mentions: OAI.Tingley.UnitSphere
def OAI.Tingley.sRadius line 83
def OAI.Tingley.wDirection line 87
Source documentation
The image-side outward unit direction.
```
def wDirection (v : UnitSphere X) : UnitSphere Y :=
…
```
Mentions: OAI.Tingley.UnitSphere
def OAI.Tingley.uRadius line 92
Source documentation
The second radial contact uses the negative of the actual direction w.
```
def uRadius (v : UnitSphere X) : ℝ :=
…
```
Mentions: OAI.Tingley.UnitSphere
def OAI.Tingley.zPoint line 96
def OAI.Tingley.rRadius line 100
def OAI.Tingley.returnSphere line 104
Source documentation
The genuine return map on the unit sphere.
```
def returnSphere (v : UnitSphere X) : UnitSphere X :=
…
```
Mentions: OAI.Tingley.UnitSphere
theorem OAI.Tingley.pRadius_pos line 109
theorem OAI.Tingley.pRadius_bounds line 113
theorem OAI.Tingley.sRadius_bounds line 118
theorem OAI.Tingley.sRadius_pos line 122
theorem OAI.Tingley.uRadius_pos line 125
theorem OAI.Tingley.uRadius_bounds line 129
theorem OAI.Tingley.rRadius_bounds line 135
theorem OAI.Tingley.rRadius_pos line 139
theorem OAI.Tingley.radii_pos line 142
theorem OAI.Tingley.radii_bounds line 148
theorem OAI.Tingley.xPoint_eq line 157
theorem OAI.Tingley.fxPoint_eq line 160
theorem OAI.Tingley.fzPoint_eq line 169
theorem OAI.Tingley.zPoint_eq line 175
theorem OAI.Tingley.norm_xPoint_sub_center line 187
theorem OAI.Tingley.norm_fxPoint_sub_center line 192
theorem OAI.Tingley.norm_zPoint_sub_center line 195
theorem OAI.Tingley.pRadius_normalize_sub line 200
Source documentation
Radial uniqueness recovers any given unit endpoint from its direction.
```
theorem pRadius_normalize_sub (x : UnitSphere X) :
    pRadius f y t ht (normalize ((x : X) - t • (y : X))
      (unit_sub_center_ne_zero x y t ht)) = ‖(x : X) - t • (y : X)‖ := by
…
```
Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.pRadius, OAI.Tingley.normalize, OAI.Tingley.unit_sub_center_ne_zero
theorem OAI.Tingley.xPoint_normalize_sub line 211
theorem OAI.Tingley.xPoint_surjective line 219

theorem OAI.Tingley.continuous_normalize_map line 225

Source documentation

Normalizing a continuous everywhere-nonzero map preserves continuity.

theorem continuous_normalize_map {A : Type*} [TopologicalSpace A]
    (g : A → X) (hg : Continuous g) (hzero : ∀ a, g a ≠ 0) :
    Continuous (fun a => normalize (g a) (hzero a)) := by
…

Mentions: OAI.Tingley.normalize

theorem OAI.Tingley.continuous_pRadius line 231
theorem OAI.Tingley.continuous_xPoint line 235
theorem OAI.Tingley.continuous_sRadius line 238
theorem OAI.Tingley.continuous_wDirection line 242
theorem OAI.Tingley.continuous_uRadius line 248
theorem OAI.Tingley.continuous_zPoint line 252
theorem OAI.Tingley.continuous_rRadius line 257
theorem OAI.Tingley.continuous_returnSphere line 260
def OAI.Tingley.pAmbient line 266
Source documentation
Total ambient functions, used only on the sphere by the convex-set argument.
```
def pAmbient (v : X) : ℝ :=
…
```
def OAI.Tingley.sAmbient line 269
def OAI.Tingley.uAmbient line 272
def OAI.Tingley.rAmbient line 275
def OAI.Tingley.returnAmbient line 278
theorem OAI.Tingley.pAmbient_coe line 282
theorem OAI.Tingley.sAmbient_coe line 286
theorem OAI.Tingley.uAmbient_coe line 290
theorem OAI.Tingley.rAmbient_coe line 294
theorem OAI.Tingley.returnAmbient_coe line 298
theorem OAI.Tingley.continuousOn_pAmbient line 303
theorem OAI.Tingley.continuousOn_sAmbient line 312
theorem OAI.Tingley.continuousOn_uAmbient line 321
theorem OAI.Tingley.continuousOn_rAmbient line 330
theorem OAI.Tingley.continuousOn_returnAmbient line 339