OAI/Geometry/PrescribedRicci/MongeAmpereMoments.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Monge Ampere Moments.

  1. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.powerIntegral line 21
  2. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.powerMoment line 23
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.powerIntegrand_continuous line 27
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.powerIntegral_nonneg line 31
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.powerMoment_nonneg line 34
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.moserPower_lpNorm_sq line 37
  7. theorem OAI.Anticanonical.SourceSmooth.KaehlerMetric.mongeAmpere_moment_step line 55
  8. theorem OAI.Anticanonical.SourceSmooth.KaehlerMetric.mongeAmpere_moment_bounds line 102