OAI/Geometry/PrescribedPotential/CalabiRicciContraction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Calabi Ricci Contraction.

  1. lemma OAI.KaehlerCalculus.LocalKaehlerField.lower_curvature_formula line 16
  2. lemma OAI.KaehlerCalculus.LocalKaehlerField.lower_curvature_symmetry line 24
  3. lemma OAI.KaehlerCalculus.LocalKaehlerField.ricciHessian_contraction line 45
  4. lemma OAI.KaehlerCalculus.LocalKaehlerField.curvature_contraction line 64
  5. lemma OAI.KaehlerCalculus.LocalKaehlerField.connection_hol_derivative line 71
  6. lemma OAI.KaehlerCalculus.LocalKaehlerField.connection_hol_flat line 82