OAI/Analysis/Mahler/SpecialJacobian.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.specialRowFactor line 12
2. def OAI.SymmetricMahler.specialDerivative line 16
3. theorem OAI.SymmetricMahler.hasFDerivAt_specialMap line 21

   Source documentation

   The actual holomorphic derivative, with its full m and h' factors.

   theorem hasFDerivAt_specialMap (A : Matrix (Fin N) (Fin n) ℝ) (m : ℕ)
       {z : Fin n → ℂ} (hz : z ∈ complexStripDomain A) :
       HasFDerivAt (specialMap A m) (specialDerivative A m z) z := by
   …

   Mentions: OAI.SymmetricMahler.complexStripDomain, OAI.SymmetricMahler.specialMap, OAI.SymmetricMahler.specialDerivative

4. def OAI.SymmetricMahler.specialJacobianMatrix line 38
5. lemma OAI.SymmetricMahler.specialJacobianMatrix_derivative line 41
6. lemma OAI.SymmetricMahler.specialRowFactor_normSq line 46
7. theorem OAI.SymmetricMahler.specialJacobian_gram line 60