OAI/Geometry/PrescribedRicci/CalabiTensorMetric.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Calabi Tensor Metric.

  1. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.calabiTensor line 18
  2. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.calabiMetric line 21
  3. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.calabiConnection line 24
  4. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.calabiNorm line 27
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.calabiTensor_smooth line 30
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.calabiMetric_posDef line 35
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.calabiNorm_nonneg line 39
  8. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.calabiMetric_smooth line 43
  9. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.calabiConnection_smooth line 53
  10. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.calabiNorm_smooth line 62
  11. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.metric_hol_connection line 68
  12. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.inverse_metric_hol_connection line 76
  13. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.calabiMetric_hol line 88
  14. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.calabiMetric_bar line 104