OAI/Geometry/PrescribedPotential/LiteralWeakHessian.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Literal Weak Hessian.

  1. def OAI.SobolevChart.schwartzCoordLinear line 21
  2. def OAI.GlobalElliptic.literalComplexHessian line 36
  3. lemma OAI.GlobalElliptic.literalComplexHessian_schwartz line 42
  4. lemma OAI.GlobalElliptic.literalComplexHessian_congr line 46
  5. lemma OAI.GlobalElliptic.literalComplexHessian_strong_continuous line 52
  6. def OAI.GlobalElliptic.GluingData.completedLocalize line 64
  7. lemma OAI.GlobalElliptic.GluingData.completedLocalize_embed line 69
  8. lemma OAI.GlobalElliptic.GluingData.completedLocalize_plus_two_embed line 76
  9. lemma OAI.GlobalElliptic.GluingData.completedLocalize_strong line 84
  10. lemma OAI.GlobalElliptic.GluingData.completedLocalize_plus_two_strong line 107
  11. lemma OAI.GlobalElliptic.GluingData.completedHessian_strong_localize line 131
  12. lemma OAI.GlobalElliptic.GluingData.completedHessian_literal line 167