OAI/Geometry/Kahler/BaseLogTests.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PinchedHartogs.BaseConstruction.Sphere line 17
  2. def OAI.PinchedHartogs.BaseConstruction.bracket line 19
  3. def OAI.PinchedHartogs.BaseConstruction.peakPolynomial line 21
  4. def OAI.PinchedHartogs.BaseConstruction.regularizedLog line 24
  5. def OAI.PinchedHartogs.BaseConstruction.logarithmicTest line 27
  6. def OAI.PinchedHartogs.BaseConstruction.basePotential line 30
  7. lemma OAI.PinchedHartogs.BaseConstruction.bracket_analytic line 33
  8. lemma OAI.PinchedHartogs.BaseConstruction.peakPolynomial_analytic line 36
  9. lemma OAI.PinchedHartogs.BaseConstruction.regularizedLog_eq line 43
  10. lemma OAI.PinchedHartogs.BaseConstruction.regularizedLog_zero line 47
  11. lemma OAI.PinchedHartogs.BaseConstruction.regularizedLog_contDiff line 50
  12. lemma OAI.PinchedHartogs.BaseConstruction.logarithmicTest_contDiff line 61
  13. lemma OAI.PinchedHartogs.BaseConstruction.peakPolynomial_zero line 68
  14. lemma OAI.PinchedHartogs.BaseConstruction.logarithmicTest_zero line 71
  15. lemma OAI.PinchedHartogs.BaseConstruction.peakPolynomial_homogeneous line 74
  16. lemma OAI.PinchedHartogs.BaseConstruction.regularizedLog_lipschitz_bound line 78
  17. def OAI.PinchedHartogs.BaseConstruction.regularizedFiberLog line 94
  18. lemma OAI.PinchedHartogs.BaseConstruction.regularizedFiberLog_contDiff line 97
  19. lemma OAI.PinchedHartogs.BaseConstruction.regularizedFiberLog_hessian line 104
  20. lemma OAI.PinchedHartogs.BaseConstruction.regularizedLog_holomorphic_psh line 131
  21. lemma OAI.PinchedHartogs.BaseConstruction.logarithmicTest_psh line 158