OAI/Geometry/PrescribedPotential/GlobalSobolev.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Global Sobolev.

  1. def OAI.GlobalElliptic.smoothSpace line 22
  2. abbrev OAI.GlobalElliptic.Smooth line 29
  3. instance OAI.GlobalElliptic.(instance at line 31) line 31
  4. lemma OAI.GlobalElliptic.Smooth.add_apply line 38
  5. lemma OAI.GlobalElliptic.Smooth.smul_apply line 39
  6. lemma OAI.GlobalElliptic.Smooth.zero_apply line 40
  7. lemma OAI.GlobalElliptic.Smooth.smooth line 42
  8. lemma OAI.GlobalElliptic.Smooth.continuous line 45
  9. lemma OAI.GlobalElliptic.Smooth.ext line 57
  10. def OAI.GlobalElliptic.Smooth.const line 59
  11. def OAI.GlobalElliptic.Smooth.mul line 62
  12. def OAI.GlobalElliptic.localizeFun line 67
  13. lemma OAI.GlobalElliptic.localizeFun_apply line 71
  14. lemma OAI.GlobalElliptic.localizeFun_support line 76
  15. lemma OAI.GlobalElliptic.localizeFun_smooth_compact line 86
  16. def OAI.GlobalElliptic.localize line 112
  17. lemma OAI.GlobalElliptic.localize_apply line 117
  18. def OAI.GlobalElliptic.localizeLinear line 122