OAI/Geometry/PrescribedPotential/GlobalHessian.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Global Hessian.

  1. lemma OAI.GlobalElliptic.cutoffGlobal_support line 26
  2. lemma OAI.GlobalElliptic.localize_cutoff_eventually line 32
  3. def OAI.GlobalElliptic.GluingData.localizedHessian line 52
  4. lemma OAI.GlobalElliptic.GluingData.localizedHessian_bound line 58
  5. lemma OAI.GlobalElliptic.GluingData.localizedHessian_source line 77
  6. def OAI.GlobalElliptic.GluingData.completedHessian line 109
  7. lemma OAI.GlobalElliptic.GluingData.completedHessian_embed line 113