OAI/Geometry/PrescribedRicci/CalabiTraceBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Calabi Trace Bound.

  1. lemma OAI.MongeAmpere.flatTensor_inv line 16
  2. lemma OAI.MongeAmpere.entrywise_norm_one_le line 23
  3. lemma OAI.MongeAmpere.flatTensor_inv_norm line 29
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.calabiNorm_le_flatEnergy line 43
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.flatTrace_lower_bound line 71
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.flatTrace_bound line 96