OAI/Analysis/Mahler/StripDifferential.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.rowCLM line 14
2. lemma OAI.SymmetricMahler.rowCLM_apply line 17
3. def OAI.SymmetricMahler.stripCoordinateCLM line 21
4. lemma OAI.SymmetricMahler.stripCoordinateCLM_apply line 26
5. def OAI.SymmetricMahler.planarDifferential line 30
6. lemma OAI.SymmetricMahler.planarDifferential_I line 33
7. def OAI.SymmetricMahler.stripDerivative line 44
8. theorem OAI.SymmetricMahler.hasFDerivAt_stripMap line 51

   Source documentation

   The full actual real derivative; its mixed x-derivative is retained.

   theorem hasFDerivAt_stripMap (A : Matrix (Fin N) (Fin n) ℝ) (m : ℕ)
       {z : (Fin n → ℝ) × (Fin n → ℝ)} (hz : z ∈ stripDomain A) :
       HasFDerivAt (stripMap A m) (stripDerivative A m z) z := by
   …

   Mentions: OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripMap, OAI.SymmetricMahler.stripDerivative