OAI/Geometry/PrescribedRicci/MongeAmpereEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Monge Ampere Energy.

  1. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_sub line 23
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_mono line 30
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_zero line 37
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.cofactorQuadratic_eq_gradientPair line 40
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.energy_segment_coercive line 52
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_energy_segment_coercive line 88
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_energy_half_segment line 105
  8. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.potentialDensity_smul_zero line 117
  9. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.potentialDensity_smul_one line 125
  10. theorem OAI.Anticanonical.SourceSmooth.KaehlerMetric.mongeAmpere_energy line 134
  11. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.mongeAmpere_energy_density_bound line 172