OAI/Geometry/Kahler/HartogsGauge.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PinchedHartogs.dz_re_holomorphic line 14
  2. lemma OAI.PinchedHartogs.dbar_re_holomorphic line 30
  3. lemma OAI.PinchedHartogs.dz_analyticAt line 36
  4. lemma OAI.PinchedHartogs.complexHessian_re_holomorphic line 43
  5. lemma OAI.PinchedHartogs.complexHessian_congr line 59
  6. lemma OAI.PinchedHartogs.complexHessian_gauge line 68
  7. def OAI.PinchedHartogs.horizontalCoordinate line 81
  8. lemma OAI.PinchedHartogs.horizontalCoordinate_apply line 86
  9. lemma OAI.PinchedHartogs.horizontalCoordinate_coordVector line 89
  10. lemma OAI.PinchedHartogs.dz_horizontal line 93
  11. def OAI.PinchedHartogs.gaugePolynomial line 97
  12. lemma OAI.PinchedHartogs.gaugePolynomial_analytic line 100
  13. lemma OAI.PinchedHartogs.gaugePolynomial_center line 112
  14. lemma OAI.PinchedHartogs.dz_gaugePolynomial line 115
  15. lemma OAI.PinchedHartogs.dz_gaugePolynomial_center line 126
  16. lemma OAI.PinchedHartogs.dz_dz_gaugePolynomial line 131
  17. lemma OAI.PinchedHartogs.dz_sub line 143
  18. lemma OAI.PinchedHartogs.dz_gauge line 149
  19. lemma OAI.PinchedHartogs.dz_dz_gauge line 160
  20. def OAI.PinchedHartogs.firstGaugeJet line 171
  21. def OAI.PinchedHartogs.secondGaugeJet line 174
  22. def OAI.PinchedHartogs.gaugedWeight line 177
  23. lemma OAI.PinchedHartogs.secondGaugeJet_symm line 180
  24. lemma OAI.PinchedHartogs.gaugedWeight_first_horizontal line 184
  25. lemma OAI.PinchedHartogs.gaugedWeight_second_horizontal line 192
  26. def OAI.PinchedHartogs.fiberGaugeMap line 200
  27. def OAI.PinchedHartogs.gaugeLogParameter line 203
  28. lemma OAI.PinchedHartogs.fiberGaugeMap_analyticAt line 206
  29. lemma OAI.PinchedHartogs.fiberGaugeMap_center line 215
  30. lemma OAI.PinchedHartogs.metricPotential_fiberGauge line 220
  31. lemma OAI.PinchedHartogs.gaugeLogParameter_neg line 230
  32. lemma OAI.PinchedHartogs.jacobianMatrix_det_of_fderiv_injective line 240
  33. lemma OAI.PinchedHartogs.fderiv_fiberGaugeMap line 251
  34. lemma OAI.PinchedHartogs.fderiv_gaugePolynomial_vertical line 264
  35. lemma OAI.PinchedHartogs.fderiv_fiberGaugeMap_injective line 275
  36. lemma OAI.PinchedHartogs.psi_chart_hessian_eventually line 297