OAI/Geometry/Kahler/HartogsCurvature.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PinchedHartogs.coordinates_complex_smul line 15
  2. lemma OAI.PinchedHartogs.complex_direction_algebra line 20
  3. lemma OAI.PinchedHartogs.anticomplex_direction_algebra line 26
  4. lemma OAI.PinchedHartogs.fderiv_complex_direction line 32
  5. lemma OAI.PinchedHartogs.fderiv_anticomplex_direction line 42
  6. def OAI.PinchedHartogs.complexJacobian line 52
  7. lemma OAI.PinchedHartogs.dz_comp_holomorphic line 55
  8. lemma OAI.PinchedHartogs.dbar_comp_holomorphic line 64
  9. lemma OAI.PinchedHartogs.dz_holomorphic line 73
  10. lemma OAI.PinchedHartogs.dbar_holomorphic line 79
  11. lemma OAI.PinchedHartogs.dz_sum line 85
  12. lemma OAI.PinchedHartogs.dbar_sum line 91
  13. lemma OAI.PinchedHartogs.complexJacobian_analyticAt line 97
  14. lemma OAI.PinchedHartogs.complexHessian_comp_holomorphic line 105
  15. def OAI.PinchedHartogs.dzMatrix line 146
  16. def OAI.PinchedHartogs.dbarMatrix line 148
  17. lemma OAI.PinchedHartogs.matrix_diff_entry line 151
  18. lemma OAI.PinchedHartogs.matrix_diff_mul line 156
  19. lemma OAI.PinchedHartogs.dzMatrix_mul line 166
  20. lemma OAI.PinchedHartogs.dbarMatrix_mul line 181
  21. lemma OAI.PinchedHartogs.dbarMatrix_add line 196
  22. lemma OAI.PinchedHartogs.dzMatrix_congr line 202
  23. lemma OAI.PinchedHartogs.dbarMatrix_congr line 207
  24. lemma OAI.PinchedHartogs.matrix_contDiffAt_dz line 212
  25. lemma OAI.PinchedHartogs.matrix_contDiffAt_dbar line 221
  26. def OAI.PinchedHartogs.curvatureMatrix line 230
  27. lemma OAI.PinchedHartogs.curvatureMatrix_apply line 233
  28. lemma OAI.PinchedHartogs.gauge_curvature_algebra line 245
  29. lemma OAI.PinchedHartogs.curvatureMatrix_gauge line 260
  30. lemma OAI.PinchedHartogs.dbarMatrix_smul line 314
  31. lemma OAI.PinchedHartogs.dbarMatrix_sum line 320
  32. lemma OAI.PinchedHartogs.dzMatrix_comp_holomorphic line 327
  33. lemma OAI.PinchedHartogs.dbarMatrix_comp_holomorphic line 334
  34. lemma OAI.PinchedHartogs.curvatureMatrix_comp_holomorphic line 341
  35. def OAI.PinchedHartogs.jacobianMatrix line 387
  36. def OAI.PinchedHartogs.pullbackMetric line 390
  37. lemma OAI.PinchedHartogs.complexHessian_pullback line 393
  38. lemma OAI.PinchedHartogs.curvatureMatrix_pullback line 407
  39. def OAI.PinchedHartogs.matrixPush line 448
  40. def OAI.PinchedHartogs.matrixPull line 451
  41. lemma OAI.PinchedHartogs.hermitianValue_dot line 453
  42. lemma OAI.PinchedHartogs.hermitianValue_matrixPull line 462
  43. lemma OAI.PinchedHartogs.matrixPull_apply line 468
  44. lemma OAI.PinchedHartogs.hermitianValue_sum line 479
  45. lemma OAI.PinchedHartogs.coordinates_complex_decomposition line 489
  46. lemma OAI.PinchedHartogs.matrixPush_jacobian line 496
  47. def OAI.PinchedHartogs.tensorPairMatrix line 509
  48. lemma OAI.PinchedHartogs.tensorValue_as_hermitianValue line 512
  49. lemma OAI.PinchedHartogs.tensorPairMatrix_curvature_apply line 525
  50. lemma OAI.PinchedHartogs.tensorPairMatrix_pullback line 533
  51. lemma OAI.PinchedHartogs.tensorValue_curvature_pullback line 553
  52. lemma OAI.PinchedHartogs.hermitianValue_pullback line 563
  53. lemma OAI.PinchedHartogs.sectional_pullback line 569
  54. lemma OAI.PinchedHartogs.curvatureMatrix_congr line 577
  55. lemma OAI.PinchedHartogs.curvature_congr line 585
  56. lemma OAI.PinchedHartogs.sectional_congr line 590
  57. lemma OAI.PinchedHartogs.sectional_complexHessian_comp line 595
  58. lemma OAI.PinchedHartogs.fderiv_injective_of_jacobianMatrix_det line 611