OAI/Geometry/Kahler/MetricCalculus.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PinchedHartogs.dz_congr line 15
  2. lemma OAI.PinchedHartogs.dbar_congr line 19
  3. lemma OAI.PinchedHartogs.dz_add line 23
  4. lemma OAI.PinchedHartogs.dbar_add line 30
  5. lemma OAI.PinchedHartogs.dz_mul line 37
  6. lemma OAI.PinchedHartogs.dbar_mul line 45
  7. lemma OAI.PinchedHartogs.fderiv_real_cast line 53
  8. lemma OAI.PinchedHartogs.dbar_eq_star_dz_real line 57
  9. lemma OAI.PinchedHartogs.dz_real_comp line 62
  10. lemma OAI.PinchedHartogs.dbar_real_comp line 73
  11. lemma OAI.PinchedHartogs._root_.OAI.ContDiffAt.hartogs_dz line 84
  12. lemma OAI.PinchedHartogs._root_.OAI.ContDiffAt.hartogs_dbar line 92
  13. lemma OAI.PinchedHartogs._root_.OAI.ContDiffAt.hartogs_real_cast line 100
  14. lemma OAI.PinchedHartogs.complexHessian_real_comp line 104
  15. lemma OAI.PinchedHartogs.dz_const_mul line 124
  16. lemma OAI.PinchedHartogs.dbar_const_mul line 131
  17. lemma OAI.PinchedHartogs.complexHessian_add line 138
  18. lemma OAI.PinchedHartogs.complexHessian_const_mul line 153
  19. lemma OAI.PinchedHartogs.complexHessian_mul line 165
  20. lemma OAI.PinchedHartogs.dz_conj line 189
  21. lemma OAI.PinchedHartogs.dbar_conj line 197
  22. lemma OAI.PinchedHartogs.dz_fiber line 205
  23. lemma OAI.PinchedHartogs.dbar_fiber line 211
  24. lemma OAI.PinchedHartogs.dbar_fiber_norm_sq line 217
  25. lemma OAI.PinchedHartogs.dz_fiber_norm_sq line 225
  26. lemma OAI.PinchedHartogs.complexHessian_fiber_norm_sq line 234
  27. lemma OAI.PinchedHartogs.complexHessian_rexp line 244
  28. lemma OAI.PinchedHartogs.negLogOneSub_hasDerivAt line 253
  29. lemma OAI.PinchedHartogs.invOneSub_hasDerivAt line 261
  30. lemma OAI.PinchedHartogs.complexHessian_negLogOneSub line 269
  31. lemma OAI.PinchedHartogs.psi_contDiffAt line 281
  32. lemma OAI.PinchedHartogs.metricPotential_contDiffAt line 288
  33. lemma OAI.PinchedHartogs.complexHessian_contDiffAt line 298
  34. lemma OAI.PinchedHartogs.hartogsMetric_contDiffOn line 306
  35. lemma OAI.PinchedHartogs.dz_real_mul line 311
  36. lemma OAI.PinchedHartogs.dbar_real_mul line 319
  37. lemma OAI.PinchedHartogs.complexHessian_fiberPotential line 327
  38. lemma OAI.PinchedHartogs.hartogsMetric_smooth_form line 358
  39. def OAI.PinchedHartogs.dzFunctional line 384
  40. def OAI.PinchedHartogs.dbarFunctional line 388
  41. lemma OAI.PinchedHartogs.dzFunctional_apply line 392
  42. lemma OAI.PinchedHartogs.dbarFunctional_apply line 398
  43. lemma OAI.PinchedHartogs.fderiv_dz_apply line 404
  44. lemma OAI.PinchedHartogs.fderiv_dbar_apply line 420
  45. lemma OAI.PinchedHartogs.dz_dbar_comm line 436
  46. lemma OAI.PinchedHartogs.dz_dz_comm line 451
  47. lemma OAI.PinchedHartogs.complexHessian_hermitian line 466
  48. lemma OAI.PinchedHartogs.complexHessian_closed line 478
  49. lemma OAI.PinchedHartogs.hartogsMetric_hermitian line 484
  50. lemma OAI.PinchedHartogs.hartogsMetric_closed line 489
  51. def OAI.PinchedHartogs.coordinateLinearEquiv line 495
  52. def OAI.PinchedHartogs.coordinateEquiv line 513
  53. lemma OAI.PinchedHartogs.dz_linear line 515
  54. lemma OAI.PinchedHartogs.dbar_linear line 523
  55. lemma OAI.PinchedHartogs.dbar_linear_norm_sq line 531
  56. lemma OAI.PinchedHartogs.dz_linear_norm_sq line 540
  57. lemma OAI.PinchedHartogs.complexHessian_linear_norm_sq line 549
  58. def OAI.PinchedHartogs.coordCLM line 556
  59. lemma OAI.PinchedHartogs.coordCLM_apply line 559
  60. lemma OAI.PinchedHartogs.coordCLM_coordVector line 561
  61. lemma OAI.PinchedHartogs.base_norm_sq_coordinates line 565
  62. lemma OAI.PinchedHartogs.complexHessian_base_norm_sq line 570
  63. lemma OAI.PinchedHartogs.dbar_base_norm_sq line 581
  64. lemma OAI.PinchedHartogs.dz_base_norm_sq line 591
  65. lemma OAI.PinchedHartogs.dz_lift_base line 601
  66. lemma OAI.PinchedHartogs.dbar_lift_base line 608
  67. lemma OAI.PinchedHartogs._root_.OAI.ContDiffAt.hartogs_dbarBase line 615
  68. lemma OAI.PinchedHartogs.complexHessian_lift_base line 623
  69. lemma OAI.PinchedHartogs.hermitianValue_lift_base line 647
  70. lemma OAI.PinchedHartogs.hermitianValue_add line 653
  71. lemma OAI.PinchedHartogs.hermitianValue_smul line 657
  72. lemma OAI.PinchedHartogs.hermitianValue_rank_one line 661
  73. lemma OAI.PinchedHartogs.hermitianValue_rank_one_self line 667
  74. lemma OAI.PinchedHartogs.hermitianValue_base_norm_sq line 674
  75. lemma OAI.PinchedHartogs.hermitianValue_base_norm_sq_self line 679
  76. lemma OAI.PinchedHartogs.hermitianValue_psi_self line 685
  77. lemma OAI.PinchedHartogs.hermitianValue_real_smul line 716
  78. def OAI.PinchedHartogs.IsPshBase line 722
  79. lemma OAI.PinchedHartogs.hartogsMetric_value line 725
  80. lemma OAI.PinchedHartogs.hartogsMetric_positive line 775
  81. theorem OAI.PinchedHartogs.hartogsMetric_isKahler line 805
  82. lemma OAI.PinchedHartogs.coordinates_real_decomposition line 812
  83. lemma OAI.PinchedHartogs.wirtinger_pair_algebra line 821
  84. lemma OAI.PinchedHartogs.fderiv_wirtinger line 826
  85. lemma OAI.PinchedHartogs.fderiv_real_wirtinger line 835
  86. lemma OAI.PinchedHartogs.dz_psi line 843
  87. lemma OAI.PinchedHartogs.fderiv_psi line 855
  88. lemma OAI.PinchedHartogs.psi_derivative_sq_le line 871
  89. def OAI.PinchedHartogs.fiberParameter line 896
  90. def OAI.PinchedHartogs.fiberPotential line 898
  91. def OAI.PinchedHartogs.thetaValue line 900
  92. lemma OAI.PinchedHartogs.fiberPotential_contDiffAt line 904
  93. lemma OAI.PinchedHartogs.dz_fiberPotential line 910
  94. lemma OAI.PinchedHartogs.fderiv_fiberPotential line 931
  95. lemma OAI.PinchedHartogs.fiberPotential_derivative_sq_le line 949
  96. def OAI.PinchedHartogs.hartogsCompactSet line 987
  97. lemma OAI.PinchedHartogs.exp_half_sq line 990
  98. lemma OAI.PinchedHartogs.norm_exp_half_smul_sq line 995
  99. lemma OAI.PinchedHartogs.fiberParameter_exp_neg_half line 999
  100. lemma OAI.PinchedHartogs.hartogsCompactSet_subset line 1005
  101. lemma OAI.PinchedHartogs.hartogsCompactSet_isCompact line 1010
  102. lemma OAI.PinchedHartogs.hartogs_barrier_sublevels_compact line 1047
  103. lemma OAI.PinchedHartogs.coordinates_equiv line 1084
  104. lemma OAI.PinchedHartogs.coordinates_equiv_symm line 1086
  105. lemma OAI.PinchedHartogs.coordinates_zero line 1089
  106. lemma OAI.PinchedHartogs.coordinates_ne_zero line 1091
  107. lemma OAI.PinchedHartogs.matrix_isUnit_of_metric_positive line 1094
  108. lemma OAI.PinchedHartogs.matrix_det_ne_zero_of_metric_positive line 1125
  109. lemma OAI.PinchedHartogs.kahler_metric_det_ne_zero line 1129
  110. lemma OAI.PinchedHartogs.matrix_contDiffAt_det line 1133
  111. lemma OAI.PinchedHartogs.matrix_contDiffAt_inv line 1144
  112. def OAI.PinchedHartogs.geodesicAcceleration line 1164
  113. def OAI.PinchedHartogs.geodesicField line 1168
  114. lemma OAI.PinchedHartogs.christoffel_contDiffAt line 1171
  115. lemma OAI.PinchedHartogs.geodesicField_contDiffAt line 1181
  116. lemma OAI.PinchedHartogs.hermitianValue_conj line 1199
  117. lemma OAI.PinchedHartogs.christoffel_contract line 1211
  118. def OAI.PinchedHartogs.connectionCubic line 1227
  119. lemma OAI.PinchedHartogs.acceleration_contract line 1231
  120. lemma OAI.PinchedHartogs.metric_dbar_conj line 1265
  121. lemma OAI.PinchedHartogs.metric_derivative_contract line 1275
  122. def OAI.PinchedHartogs.metricEnergy line 1290
  123. lemma OAI.PinchedHartogs.metric_energy_hasDerivAt_zero line 1293
  124. lemma OAI.PinchedHartogs.geodesic_energy_hasDerivAt_zero line 1326
  125. lemma OAI.PinchedHartogs.coordinates_real_smul line 1333
  126. lemma OAI.PinchedHartogs.hermitianValue_vector_real_smul line 1338
  127. lemma OAI.PinchedHartogs.metricEnergy_nonneg line 1351
  128. lemma OAI.PinchedHartogs.metricEnergy_continuousOn line 1358
  129. lemma OAI.PinchedHartogs.compact_metric_coercivity line 1373
  130. lemma OAI.PinchedHartogs.geodesic_energy_constant line 1401
  131. lemma OAI.PinchedHartogs.hartogs_isOpen_smooth line 1412
  132. lemma OAI.PinchedHartogs.abs_le_add_one_of_sq_le line 1425
  133. lemma OAI.PinchedHartogs.curve_function_bound line 1429
  134. lemma OAI.PinchedHartogs.hartogs_geodesic_compact_containment line 1450