OAI/Geometry/PrescribedRicci/ComplexIntegrationByParts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Complex Integration By Parts.

  1. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.barDeriv line 16
  2. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.holDeriv line 20
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.contDiff_deriv_direction line 24
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.contDiff_barDeriv line 29
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.contDiff_holDeriv line 34
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.compactSupport_barDeriv line 39
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integrable_mul_deriv line 44
  8. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integrable_deriv_mul line 50
  9. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.contDiffAt_deriv_direction line 56
  10. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.continuous_mul_on_tsupport line 61
  11. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.contDiff_mul_on_tsupport line 72
  12. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integrable_mul_deriv_local line 84
  13. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integrable_deriv_mul_local line 92
  14. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.integral_mul_barDeriv_local line 100