OAI/Geometry/PrescribedPotential/RealSobolev.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Real Sobolev.

  1. lemma OAI.ClosedCore.maps_closure_range line 20
  2. def OAI.GlobalElliptic.realSmoothSpace line 33
  3. abbrev OAI.GlobalElliptic.RealSmooth line 39
  4. def OAI.GlobalElliptic.RealSmooth.ofReal line 43
  5. def OAI.GlobalElliptic.RealSmooth.source line 46
  6. lemma OAI.GlobalElliptic.RealSmooth.ofReal_source line 48
  7. def OAI.GlobalElliptic.RealSmooth.const line 53
  8. lemma OAI.GlobalElliptic.RealSmooth.complexL_real line 55
  9. def OAI.GlobalElliptic.RealSmooth.laplace line 74
  10. def OAI.GlobalElliptic.Localizers.realCoreMap line 84
  11. def OAI.GlobalElliptic.Localizers.realCompletion line 87
  12. abbrev OAI.GlobalElliptic.Localizers.RealSobolev line 90
  13. instance OAI.GlobalElliptic.Localizers.realSobolev_complete line 92
  14. def OAI.GlobalElliptic.Localizers.realEmbed line 95
  15. lemma OAI.GlobalElliptic.Localizers.realEmbed_val line 99
  16. lemma OAI.GlobalElliptic.Localizers.realEmbed_dense line 102
  17. lemma OAI.GlobalElliptic.Localizers.maps_realCompletion line 109
  18. lemma OAI.GlobalElliptic.Localizers.real_strong line 114