OAI/Geometry/PrescribedPotential/FredholmRegularity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Fredholm Regularity.

  1. lemma OAI.GlobalElliptic.Localizers.BoundedCore.add line 23
  2. lemma OAI.GlobalElliptic.Localizers.BoundedCore.smul line 32
  3. lemma OAI.GlobalElliptic.Localizers.extendCore_add line 39
  4. lemma OAI.GlobalElliptic.Localizers.extendCore_smul line 48
  5. def OAI.GlobalElliptic.GluingData.resolventZero line 61
  6. def OAI.GlobalElliptic.GluingData.feedbackCore line 65
  7. lemma OAI.GlobalElliptic.GluingData.feedbackCore_bound line 68
  8. lemma OAI.GlobalElliptic.GluingData.feedbackCore_bound_zero line 74
  9. lemma OAI.GlobalElliptic.GluingData.completed_feedback line 80
  10. theorem OAI.GlobalElliptic.GluingData.resolvent_feedback_regular line 95
  11. lemma OAI.GlobalElliptic.GluingData.smooth_shifted_equation line 115