OAI/Geometry/PrescribedRicci/LocalKahlerEnergy.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Local Kahler Energy.

  1. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.holRealForm line 15
  2. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.holRealDeriv line 22
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.contDiffAt_holRealDeriv line 25
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.fderiv_holRealDeriv line 30
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.barDeriv_holRealDeriv line 38
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.barDeriv_mul line 47
  7. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.entryCLM line 56
  8. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.fderiv_entry line 60
  9. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.barDeriv_entry line 66
  10. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.barDeriv_sum line 73
  11. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.contDiffAt_barDeriv line 80
  12. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.contDiffAt_weightedInverse_matrix line 88
  13. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.weightedInverse_entry_divergence line 96
  14. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.cofactorFlux line 105
  15. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.contDiffAt_cofactorFlux line 109
  16. theorem OAI.Anticanonical.SourceSmooth.KaehlerMetric.cofactorFlux_divergence line 119
  17. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integrable_mul_barDeriv_local line 164
  18. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integrable_barDeriv_mul_local line 178
  19. theorem OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_cofactorFlux line 192