OAI/Geometry/PrescribedPotential/PotentialDensity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Potential Density.

  1. lemma OAI.Anticanonical.SourceSmooth.hermitian_det_im line 18
  2. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumePolynomial line 27
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumePolynomial_compatibility line 31
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumePolynomial_im line 44
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumePolynomial_smooth line 53
  6. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.potentialDensityValue line 60
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.potentialDensityValue_local line 63
  8. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.potentialDensity line 69
  9. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.potentialDensity_complex line 78
  10. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.potentialDensity_directional line 85