OAI/Geometry/PrescribedPotential/VolumePath.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Volume Path.

  1. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumeCoefficient_pos line 19
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumeCoefficient_smooth line 23
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumeCoefficient_compatibility line 34
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.logVolume_compatibility line 52
  5. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.logRatioValue line 64
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.logRatioValue_local line 69
  7. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.logRatio line 78
  8. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.logRatio_local line 90
  9. def OAI.Anticanonical.SourceSmooth.prescribedForcingValue line 101
  10. lemma OAI.Anticanonical.SourceSmooth.prescribedForcingValue_local line 106
  11. def OAI.Anticanonical.SourceSmooth.prescribedForcing line 116
  12. lemma OAI.Anticanonical.SourceSmooth.prescribedForcing_local line 126
  13. def OAI.Anticanonical.SourceSmooth.SolvesVolumePath line 136
  14. lemma OAI.Anticanonical.SourceSmooth.volumePath_zero line 141
  15. lemma OAI.Anticanonical.SourceSmooth.volumePath_one line 156