OAI/Geometry/PrescribedRicci/GlobalKahlerIntegral.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Global Kahler Integral.

  1. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.localizeFunction line 20
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.localizeFunction_support line 23
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.localizeFunction_continuous_compact line 32
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.continuous_real_mul_on_tsupport line 62
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chart_integrable line 73
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chartIntegral_linear_add line 87
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chartIntegral_sum line 94
  8. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.chartPartition line 101
  9. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chartPartition_nonneg line 104
  10. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chartPartition_sum line 107
  11. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chartPartition_support line 110
  12. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral line 116
  13. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_chart line 119
  14. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_add line 138
  15. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_const_mul line 151
  16. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_sum line 161
  17. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_nonneg line 171