PoleCutoffs.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The actual north, south, and off-pole partition

The fixed ambient bumps have outer radius 1/4 and are one on radius 1/8. The remainder therefore stays a fixed distance from both stationary poles.

def OAI.Falconer.oppositePole line 18
theorem OAI.Falconer.oppositePole_coe line 21
theorem OAI.Falconer.oppositePole_opposite line 24
def OAI.Falconer.poleCutoff line 27
def OAI.Falconer.offPoleCutoff line 30
theorem OAI.Falconer.poleCutoff_contDiff line 33
theorem OAI.Falconer.offPoleCutoff_contDiff line 36
theorem OAI.Falconer.poleCutoff_one line 40
theorem OAI.Falconer.poleCutoff_zero line 48
theorem OAI.Falconer.poleCutoff_support line 53
theorem OAI.Falconer.pole_distance_sum line 58
theorem OAI.Falconer.offPoleCutoff_zero_near line 68
theorem OAI.Falconer.offPoleCutoff_opposite line 74
theorem OAI.Falconer.offPoleCutoff_gap line 80
theorem OAI.Falconer.poleCutoff_partition line 115
theorem OAI.Falconer.quadraticSpherePoint_dist_pole line 122
Source documentation
In quadratic coordinates, Euclidean distance from the pole is exactly the coordinate radius. This gives the needed interior cutoff support.
```
theorem quadraticSpherePoint_dist_pole {n : ℕ} {u : Space n} (hu : ‖u‖ ≤ 2) :
    ‖quadraticSpherePoint u-coordinateJoin (0 : Space n) 1‖ = ‖u‖ := by
…
```
Mentions: OAI.Falconer.Space, OAI.Falconer.quadraticSpherePoint, OAI.Falconer.coordinateJoin
theorem OAI.Falconer.quadraticToGnomonic_image_smallBall line 135
Source documentation
Only a small fixed part of the coordinate image is needed for the application. Radial continuity proves its inclusion without imposing a global inverse chart.
```
theorem quadraticToGnomonic_image_smallBall {n : ℕ} (x : Space n)
    (hx : ‖x‖ ≤ 1/2) :
    x ∈ quadraticToGnomonic '' ball (0 : Space n) 1 := by
…
```
Mentions: OAI.Falconer.Space, OAI.Falconer.quadraticToGnomonic