OAI/Geometry/PrescribedPotential/CalabiConnection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Calabi Connection.

  1. structure OAI.KaehlerCalculus.LocalKaehlerField line 17
  2. def OAI.KaehlerCalculus.LocalKaehlerField.connection line 31
  3. def OAI.KaehlerCalculus.LocalKaehlerField.curvature line 34
  4. def OAI.KaehlerCalculus.LocalKaehlerField.logDet line 37
  5. def OAI.KaehlerCalculus.LocalKaehlerField.ricciHessian line 39
  6. lemma OAI.KaehlerCalculus.LocalKaehlerField.inverse_smooth line 42
  7. lemma OAI.KaehlerCalculus.LocalKaehlerField.connection_smooth line 45
  8. lemma OAI.KaehlerCalculus.LocalKaehlerField.logDet_smooth line 51
  9. lemma OAI.KaehlerCalculus.LocalKaehlerField.connection_symmetric line 58
  10. lemma OAI.KaehlerCalculus.LocalKaehlerField.curvature_formula line 68
  11. lemma OAI.KaehlerCalculus.LocalKaehlerField.ricciHessian_trace line 80
  12. lemma OAI.KaehlerCalculus.LocalKaehlerField.curvature_contraction_at_one line 92