OAI/Geometry/Kahler/HartogsNormalBlocks.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PinchedHartogs.block3 line 14
  2. lemma OAI.PinchedHartogs.block3_horizontal line 17
  3. lemma OAI.PinchedHartogs.block3_vertical_left line 20
  4. lemma OAI.PinchedHartogs.block3_vertical_right line 22
  5. lemma OAI.PinchedHartogs.block3_vertical line 24
  6. lemma OAI.PinchedHartogs.block3_one line 26
  7. lemma OAI.PinchedHartogs.block3_mul line 30
  8. lemma OAI.PinchedHartogs.block3_inv line 36
  9. lemma OAI.PinchedHartogs.verticalDelta_horizontal line 42
  10. lemma OAI.PinchedHartogs.verticalDelta_vertical line 44
  11. lemma OAI.PinchedHartogs.horizontalIdentity_horizontal line 45
  12. lemma OAI.PinchedHartogs.horizontalIdentity_vertical_left line 48
  13. lemma OAI.PinchedHartogs.horizontalIdentity_vertical_right line 50
  14. lemma OAI.PinchedHartogs.normalPotential_hessian_block line 53
  15. lemma OAI.PinchedHartogs.sum_fin3_horizontal line 69
  16. lemma OAI.PinchedHartogs.block3_contraction line 73
  17. lemma OAI.PinchedHartogs.barrierX_positive line 80
  18. lemma OAI.PinchedHartogs.barrierQ_positive line 83