OAI/Geometry/PrescribedPotential/RegularityJets.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Regularity Jets.

  1. def OAI.GlobalElliptic.chartOperator line 22
  2. lemma OAI.GlobalElliptic.GluingData.chartOperator_bound line 30
  3. def OAI.GlobalElliptic.GluingData.regularityHessian line 47
  4. def OAI.GlobalElliptic.GluingData.regularityError line 50
  5. lemma OAI.GlobalElliptic.GluingData.regularityHessian_bound line 54
  6. lemma OAI.GlobalElliptic.GluingData.regularityError_bound line 61
  7. lemma OAI.GlobalElliptic.chartHessian_source line 71
  8. lemma OAI.GlobalElliptic.GluingData.regularityHessian_source line 103
  9. def OAI.GlobalElliptic.GluingData.completedRegularityHessian line 112
  10. def OAI.GlobalElliptic.GluingData.completedRegularityError line 116
  11. lemma OAI.GlobalElliptic.GluingData.completedRegularityHessian_embed line 120
  12. lemma OAI.GlobalElliptic.GluingData.completedRegularityError_embed line 125