OAI/Geometry/PrescribedPotential/CalabiCovariant.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Calabi Covariant.

  1. lemma OAI.KaehlerCalculus.LocalKaehlerField.curvature_smooth line 20
  2. lemma OAI.KaehlerCalculus.LocalKaehlerField.ricciHessian_smooth line 25
  3. def OAI.KaehlerCalculus.LocalKaehlerField.covHol line 30
  4. lemma OAI.KaehlerCalculus.LocalKaehlerField.covHol_smooth line 35
  5. lemma OAI.KaehlerCalculus.LocalKaehlerField.covHol_connection_swap line 46
  6. lemma OAI.KaehlerCalculus.LocalKaehlerField.derivative_curvature_contraction_at_one line 55
  7. lemma OAI.KaehlerCalculus.LocalKaehlerField.bar_covHol_connection line 94
  8. lemma OAI.KaehlerCalculus.LocalKaehlerField.calabi_connection_laplacian_at_one line 117