OAI/Geometry/PrescribedRicci/SmoothPositivePath.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Smooth Positive Path.

  1. def OAI.GlobalElliptic.RealSmooth.expAffine line 29
  2. lemma OAI.GlobalElliptic.RealSmooth.expAffine_apply line 34
  3. lemma OAI.GlobalElliptic.GluingData.exponentialDensity_embedViaEnergy line 48
  4. theorem OAI.GlobalElliptic.GluingData.smooth_positive_path_eventually line 69