OAI/Analysis/Mahler/StripJacobian.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SymmetricMahler.det_eq_vertical_block line 14

   Source documentation

   Determinant of a real linear map that fixes its first coordinate and has vertical block G; arbitrary mixed derivatives do not affect the determinant.

   lemma det_eq_vertical_block
       (L : ((Fin n → ℝ) × (Fin n → ℝ)) →ₗ[ℝ] ((Fin n → ℝ) × (Fin n → ℝ)))
       (G : Matrix (Fin n) (Fin n) ℝ)
       (hfst : ∀ z, (L z).1 = z.1)
       (hvertical : ∀ y, (L (0,y)).2 = G.mulVec y) : L.det = G.det := by
   …

2. lemma OAI.SymmetricMahler.stripDerivative_fst line 27
3. lemma OAI.SymmetricMahler.stripDerivative_vertical line 30
4. theorem OAI.SymmetricMahler.abs_det_stripDerivative line 52

   Source documentation

   The exact Jacobian identity for the actual derivative of the actual map.

   theorem abs_det_stripDerivative (A : Matrix (Fin N) (Fin n) ℝ) {m : ℕ} (hm : 2 ≤ m)
       {z : (Fin n → ℝ) × (Fin n → ℝ)} (hz : z ∈ stripDomain A) :
       |(stripDerivative A m z).det| = (4/(Real.pi*(m : ℝ)))^n*
         (weightedGram A (fun j => hessianWeight m (inverseF (stripCoordinate A z j))
           (deriv inverseF (stripCoordinate A z j)))).det := by
   …

   Mentions: OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripDerivative, OAI.SymmetricMahler.weightedGram, OAI.SymmetricMahler.hessianWeight, OAI.SymmetricMahler.stripCoordinate