OAI/Geometry/PrescribedPotential/SmoothPathLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Smooth Path Limit.

  1. lemma OAI.Anticanonical.SourceSmooth.solvesVolumePath_density line 25
  2. lemma OAI.Anticanonical.SourceSmooth.solvesVolumePath_of_density line 33
  3. lemma OAI.GlobalElliptic.GluingData.realMatrix_tendsto line 52
  4. lemma OAI.GlobalElliptic.GluingData.completedVolume_realSmooth_embed line 63
  5. lemma OAI.GlobalElliptic.GluingData.potentialDensity_tendsto line 69
  6. lemma OAI.GlobalElliptic.GluingData.positivePotential_of_smooth_limit line 89
  7. theorem OAI.GlobalElliptic.GluingData.smooth_path_limit_solution line 113