OAI/Geometry/PrescribedRicci/KaehlerTrace.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Kaehler Trace.

  1. lemma OAI.MongeAmpere.trace_mul_pos line 14
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.traceMetric_compatibility line 34
  3. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.traceMetricValue line 49
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.traceMetricValue_local line 53
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.traceMetric_local_smooth line 58
  6. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.traceMetric line 70
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.traceMetric_local line 78
  8. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.traceMetric_pos line 84
  9. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.laplacian_deform line 93