OAI/Geometry/PrescribedRicci/MongeAmperePowerEnergy.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Monge Ampere Power Energy.

  1. def OAI.Anticanonical.SourceSmooth.powerBase line 17
  2. lemma OAI.Anticanonical.SourceSmooth.powerBase_pos line 18
  3. lemma OAI.Anticanonical.SourceSmooth.powerBase_smooth line 19
  4. lemma OAI.Anticanonical.SourceSmooth.powerBase_deriv line 20
  5. def OAI.Anticanonical.SourceSmooth.moserTest line 23
  6. def OAI.Anticanonical.SourceSmooth.moserPower line 24
  7. lemma OAI.Anticanonical.SourceSmooth.moserTest_smooth line 26
  8. lemma OAI.Anticanonical.SourceSmooth.moserPower_smooth line 28
  9. lemma OAI.Anticanonical.SourceSmooth.moserTest_deriv line 31
  10. lemma OAI.Anticanonical.SourceSmooth.moserPower_deriv line 39
  11. lemma OAI.Anticanonical.SourceSmooth.moserTest_deriv_lower line 46
  12. lemma OAI.Anticanonical.SourceSmooth.moserTest_deriv_nonneg line 53
  13. lemma OAI.Anticanonical.SourceSmooth.moserPower_deriv_sq_le line 57
  14. lemma OAI.Anticanonical.SourceSmooth.abs_moserTest_le line 75
  15. lemma OAI.Anticanonical.SourceSmooth.moserPower_sq line 91
  16. lemma OAI.Anticanonical.SourceSmooth.moserPower_rpow line 96
  17. theorem OAI.Anticanonical.SourceSmooth.KaehlerMetric.mongeAmpere_power_energy line 106