OAI/Geometry/PrescribedPotential/CompletedResolvent.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Completed Resolvent.

  1. lemma OAI.GlobalElliptic.Localizers.extendCore_compat line 27
  2. def OAI.GlobalElliptic.Localizers.AllRegular line 36
  3. lemma OAI.GlobalElliptic.Localizers.allRegular_embed line 39
  4. lemma OAI.GlobalElliptic.Localizers.allRegular_of_gain line 43
  5. def OAI.GlobalElliptic.GluingData.completedL line 66
  6. def OAI.GlobalElliptic.GluingData.shiftedOperator line 69
  7. def OAI.GlobalElliptic.GluingData.completedParametrix line 72
  8. def OAI.GlobalElliptic.GluingData.completedError line 76
  9. lemma OAI.GlobalElliptic.GluingData.completedParametrix_bound line 80
  10. lemma OAI.GlobalElliptic.GluingData.completedParametrix_equation line 86
  11. lemma OAI.GlobalElliptic.GluingData.exists_completedError_small line 101
  12. def OAI.GlobalElliptic.GluingData.errorInverse line 108
  13. lemma OAI.GlobalElliptic.GluingData.errorInverse_equation line 112
  14. def OAI.GlobalElliptic.GluingData.completedResolvent line 119
  15. theorem OAI.GlobalElliptic.GluingData.completedResolvent_equation line 123
  16. lemma OAI.GlobalElliptic.GluingData.errorInverse_regular line 129
  17. lemma OAI.GlobalElliptic.GluingData.parametrix_regular line 135
  18. theorem OAI.GlobalElliptic.GluingData.completedResolvent_regular line 152