OAI/Geometry/PrescribedRicci/CompactPathRicci.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compact Path Ricci.

  1. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumePath_holDerivative_congr line 21
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.holDerivative_sub_smul line 25
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumePath_ricci_hol line 37
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumePath_ricci_bounds_on_compact line 52