OAI/Geometry/PrescribedRicci/KahlerGradientEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Kahler Gradient Energy.

  1. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.barDeriv_congr line 14
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.barDeriv_add line 19
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.barDeriv_ofReal line 27
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.holRealDeriv_mul line 36
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.potentialMatrix_mul line 44
  6. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.gradientPair line 72
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.gradientPair_star line 75
  8. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.gradientPair_self_nonneg line 89
  9. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.trace_hessian_product line 102