QuadraticChart.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The fixed quadratic chart at a sphere pole

This is the actual chart in osc:stationary. Its phase is exactly quadratic, in every dimension. Surface measure transport and its Jacobian are separate from the geometric statements here.

def OAI.Falconer.quadraticSpherePoint line 20
theorem OAI.Falconer.quadraticSpherePoint_zero_coord line 23
theorem OAI.Falconer.quadraticSpherePoint_succ_coord line 27
theorem OAI.Falconer.quadraticSpherePoint_norm line 31
def OAI.Falconer.quadraticSphereChart line 41
theorem OAI.Falconer.quadraticSpherePoint_phase line 50
Source documentation
The oscillatory phase at the pole is exactly 1 - ‖u‖²/2.
```
theorem quadraticSpherePoint_phase {n : ℕ} (u : Space n) :
    inner ℝ (quadraticSpherePoint u) (coordinateJoin (0 : Space n) 1) =
      1-‖u‖^2/2 := by
…
```
Mentions: OAI.Falconer.Space, OAI.Falconer.quadraticSpherePoint, OAI.Falconer.coordinateJoin
theorem OAI.Falconer.quadraticSpherePoint_contDiffAt line 55
theorem OAI.Falconer.quadraticSphereChart_mem_hemisphere line 69
def OAI.Falconer.quadraticToGnomonic line 80
Source documentation
The exact change from quadratic coordinates to the existing gnomonic coordinates. On the unit ball its denominator is bounded away from zero.
```
noncomputable def quadraticToGnomonic {n : ℕ} (u : Space n) : Space n :=
…
```
Mentions: OAI.Falconer.Space
theorem OAI.Falconer.gnomonicChart_quadraticToGnomonic line 83
theorem OAI.Falconer.quadraticToGnomonic_injOn line 106