OAI/Geometry/PrescribedPotential/EvenRellich.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Even Rellich.

  1. def OAI.GlobalElliptic.GluingData.shiftedOrder line 26
  2. lemma OAI.GlobalElliptic.GluingData.shiftedOrder_embed line 30
  3. lemma OAI.GlobalElliptic.GluingData.shiftedOrder_lower line 37
  4. lemma OAI.GlobalElliptic.GluingData.resolventOrder_left line 46
  5. lemma OAI.GlobalElliptic.GluingData.lower_resolvent_factor line 55
  6. lemma OAI.GlobalElliptic.GluingData.lower_compact_step line 74
  7. def OAI.GlobalElliptic.GluingData.CompactLower line 85
  8. theorem OAI.GlobalElliptic.GluingData.lower_even_compact line 88