OAI/Geometry/PrescribedPotential/PositivePotentialLinearization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positive Potential Linearization.

  1. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.potentialDensity_quotient line 22
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.potentialDensity_pos line 39
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.potentialLogDensity_directional line 48
  4. theorem OAI.Anticanonical.SourceSmooth.positivePotential_linearized_solvable line 91