OAI/Geometry/Kahler/HartogsNormalTables.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PinchedHartogs.verticalDelta line 14
  2. def OAI.PinchedHartogs.liftedHessian line 16
  3. def OAI.PinchedHartogs.liftedThird line 19
  4. def OAI.PinchedHartogs.liftedBarThird line 22
  5. def OAI.PinchedHartogs.liftedFourth line 25
  6. lemma OAI.PinchedHartogs.dz_dbar_congr line 28
  7. lemma OAI.PinchedHartogs.dbar_dz_congr line 34
  8. lemma OAI.PinchedHartogs.normalLogWeight_third line 40
  9. lemma OAI.PinchedHartogs.normalLogWeight_barThird line 48
  10. lemma OAI.PinchedHartogs.normalLogWeight_fourth line 56
  11. lemma OAI.PinchedHartogs.normalBarrier_hessian line 64
  12. lemma OAI.PinchedHartogs.normalBarrier_third line 74
  13. lemma OAI.PinchedHartogs.normalBarrier_fourth line 88