OAI/Geometry/PrescribedPotential/WirtingerCalculus.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Wirtinger Calculus.

  1. abbrev OAI.KaehlerCalculus.V line 17
  2. def OAI.KaehlerCalculus.wderiv line 19
  3. def OAI.KaehlerCalculus.dz line 22
  4. def OAI.KaehlerCalculus.dzbar line 23
  5. lemma OAI.KaehlerCalculus.wderiv_smooth line 25
  6. lemma OAI.KaehlerCalculus.wderiv_congr line 32
  7. lemma OAI.KaehlerCalculus.wderiv_add line 36
  8. lemma OAI.KaehlerCalculus.wderiv_const_mul line 42
  9. lemma OAI.KaehlerCalculus.wderiv_mul line 48
  10. lemma OAI.KaehlerCalculus.wderiv_const line 56
  11. lemma OAI.KaehlerCalculus.fderiv_wderiv line 59
  12. lemma OAI.KaehlerCalculus.wderiv_comm line 74
  13. lemma OAI.KaehlerCalculus.fderiv_ofReal line 83
  14. lemma OAI.KaehlerCalculus.snd_fderiv_ofReal line 89
  15. lemma OAI.KaehlerCalculus.dzbar_dz_real line 103
  16. lemma OAI.KaehlerCalculus.potentialMatrix_eq_dzbar_dz line 111