OAI/Geometry/PrescribedRicci/KahlerVolumeMeasure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Kahler Volume Measure.

  1. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.integralPositive line 20
  2. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumeMeasure line 28
  3. instance OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumeMeasure_regular line 31
  4. instance OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumeMeasure_finite line 35
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_volumeMeasure line 39