OAI/Geometry/PrescribedPotential/LocalizedCompact.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Localized Compact.

  1. def OAI.EllipticCompact.localizedFun line 20
  2. lemma OAI.EllipticCompact.localizedFun_bound line 24
  3. lemma OAI.EllipticCompact.localizedFun_memLp line 33
  4. def OAI.EllipticCompact.localizedLp line 42
  5. lemma OAI.EllipticCompact.localizedLp_ae line 45
  6. lemma OAI.EllipticCompact.localizedLp_norm line 49
  7. def OAI.EllipticCompact.localizeLinear line 59
  8. def OAI.EllipticCompact.localizeL2 line 83
  9. lemma OAI.EllipticCompact.localizeL2_ae line 88
  10. lemma OAI.EllipticCompact.localizeL2_restrict line 92