OAI/Geometry/PrescribedRicci/KahlerCauchySchwarz.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Kahler Cauchy Schwarz.

  1. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.energy_realSMul_left line 23
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.energy_constant_left line 30
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_laplacian line 37
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_cauchySchwarz line 45
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.energy_add_right line 70
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.energy_realSMul_right line 76
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.energy_cauchySchwarz line 80