OAI/Geometry/Kahler/HartogsNormalJets.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PinchedHartogs._root_.OAI.ContDiffAt.hartogs_dzBase line 14
  2. lemma OAI.PinchedHartogs.dz_dz_lift_base line 22
  3. lemma OAI.PinchedHartogs.dz_gaugePolynomial_vertical line 41
  4. lemma OAI.PinchedHartogs.dz_dz_gaugePolynomial_vertical_right line 46
  5. lemma OAI.PinchedHartogs.dz_dz_gaugePolynomial_vertical_left line 51
  6. lemma OAI.PinchedHartogs.dz_dz_gaugePolynomial_all line 56
  7. def OAI.PinchedHartogs.baseGaugePolynomial line 71
  8. def OAI.PinchedHartogs.normalLogWeight line 75
  9. lemma OAI.PinchedHartogs.baseGaugePolynomial_analytic line 78
  10. lemma OAI.PinchedHartogs.normalLogWeight_contDiffAt line 81
  11. lemma OAI.PinchedHartogs.normalLogWeight_hessian line 88
  12. lemma OAI.PinchedHartogs.normalLogWeight_first line 94
  13. lemma OAI.PinchedHartogs.normalLogWeight_pureSecond line 114
  14. lemma OAI.PinchedHartogs.normalLogWeight_hessian_eventually line 139
  15. lemma OAI.PinchedHartogs.dbar_dz_dz_real line 146
  16. lemma OAI.PinchedHartogs.dbar_dbar_real line 155
  17. lemma OAI.PinchedHartogs.normalLogWeight_barFirst line 166
  18. lemma OAI.PinchedHartogs.normalLogWeight_pureBarSecond line 173