OAI/Geometry/PrescribedPotential/SmoothPathOpenness.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Smooth Path Openness.

  1. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.logRatio_deform_eq_logDensity line 24
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.positivePotential_add line 34
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.logRatio_deform_add line 41
  4. theorem OAI.Anticanonical.SourceSmooth.smooth_log_path_eventually_solvable line 58
  5. def OAI.Anticanonical.SourceSmooth.SmoothVolumePathTimes line 73
  6. lemma OAI.Anticanonical.SourceSmooth.smoothVolumePathTimes_zero line 77
  7. lemma OAI.Anticanonical.SourceSmooth.smoothVolumePathTimes_eventually line 81
  8. theorem OAI.Anticanonical.SourceSmooth.smoothVolumePathTimes_isOpen line 101