OAI/Geometry/PrescribedPotential/SobolevExponential.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Sobolev Exponential.

  1. lemma OAI.ExponentialEvaluation.apply_exp line 20
  2. def OAI.ExponentialEvaluation.orbit line 45
  3. lemma OAI.ExponentialEvaluation.orbit_zero line 49
  4. lemma OAI.ExponentialEvaluation.orbit_continuous line 52
  5. def OAI.GlobalElliptic.RealSmooth.mul line 65
  6. def OAI.GlobalElliptic.GluingData.realMultiplier line 82
  7. lemma OAI.GlobalElliptic.GluingData.realMultiplier_evaluation line 90
  8. def OAI.GlobalElliptic.GluingData.exponentialDensity line 106
  9. lemma OAI.GlobalElliptic.GluingData.exponentialDensity_zero line 110
  10. lemma OAI.GlobalElliptic.GluingData.exponentialDensity_continuous line 114
  11. lemma OAI.GlobalElliptic.GluingData.exponentialDensity_strong line 118