QuadraticJacobian.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The Jacobian of the quadratic-to-gnomonic change of variables

The matrix determinant lemma applies to the actual derivative, a scalar matrix plus one radial term. This gives the measure Jacobian needed to transfer the published gnomonic density to the quadratic chart.

theorem OAI.Falconer.radial_matrix_det line 18
theorem OAI.Falconer.quadraticCoordinateDifferential_det line 37
theorem OAI.Falconer.radial_det_factor line 69
theorem OAI.Falconer.radial_quotient_factor line 74
theorem OAI.Falconer.quadraticCoordinateDifferential_det_explicit line 83
Source documentation
The dimension range in which the published gnomonic formula is used. The ambient dimension is m+3 and the sphere dimension is m+2.
```
theorem quadraticCoordinateDifferential_det_explicit (m : ℕ) {u : Space (m+2)}
    (hu : ‖u‖ < 1) :
    (quadraticCoordinateDifferential u).det =
      (Real.sqrt (1-‖u‖^2/4))^m / (1-‖u‖^2/2)^(m+3) := by
…
```
Mentions: OAI.Falconer.Space, OAI.Falconer.quadraticCoordinateDifferential
theorem OAI.Falconer.quadraticCoordinateDifferential_det_pos line 100