OAI/Analysis/Mahler/HemisphereJacobian.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MahlerStokes.splitCoordinate line 12

   Source documentation

   Move the distinguished coordinate first without changing the relative order of any other coordinates. The same reindexing is used on both matrix axes.

   def splitCoordinate {n : ℕ} (i : Fin (n+1)) : Fin 1 ⊕ Fin n ≃ Fin (n+1) :=
   …

2. def OAI.MahlerStokes.hemisphereFrameMatrix line 24
3. lemma OAI.MahlerStokes.splitCoordinate_inl line 29
4. lemma OAI.MahlerStokes.splitCoordinate_inr line 32
5. lemma OAI.MahlerStokes.det_hemisphereFrameMatrix line 35
6. lemma OAI.MahlerStokes.hemisphereConeDerivative_matrix line 54
7. theorem OAI.MahlerStokes.det_hemisphereConeDerivative line 71

   Source documentation

   The actual ambient Jacobian of radial hemisphere coordinates. The singularity is only at the equator, outside the open parameter domain.

   theorem det_hemisphereConeDerivative {n : ℕ} (i : Fin (n+1))
       {x : Fin (n+1) → ℝ} (hx : x ∈ hemisphereConeDomain i) :
       (hemisphereConeDerivative i x).toLinearMap.det =
         (x i)^n * (chord 1 (i.removeNth x))⁻¹ := by
   …

   Mentions: OAI.MahlerStokes.hemisphereConeDomain, OAI.MahlerStokes.hemisphereConeDerivative, OAI.MahlerStokes.chord