OAI/Geometry/PrescribedRicci/KahlerChartLp.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Kahler Chart Lp.

  1. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chart_integral_upper line 20
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.tsupport_norm_rpow line 46
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.localize_norm_rpow line 55
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chart_lpNorm_bound line 62