OAI/Geometry/PrescribedRicci/CalabiTrace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Calabi Trace.

  1. lemma OAI.MongeAmpere.hermPair_kronecker_one_trace line 17
  2. lemma OAI.MongeAmpere.trace_real line 30
  3. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.flatTrace line 44
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.flatTrace_smooth line 47
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.flatTrace_hol line 53
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.flatTrace_hessian line 63
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.flatTrace_laplacian line 85