OAI/Geometry/TamingCompatibility/Elliptic/SobolevBounded.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.EuclideanSobolev.boundedToLpTop line 20
  2. lemma OAI.TamingCompatibility.EuclideanSobolev.boundedToLpTop_injective line 43
  3. def OAI.TamingCompatibility.EuclideanSobolev.boundedDistributionCLM line 50
  4. lemma OAI.TamingCompatibility.EuclideanSobolev.boundedDistributionCLM_apply line 53
  5. lemma OAI.TamingCompatibility.EuclideanSobolev.boundedDistributionCLM_injective line 56
  6. def OAI.TamingCompatibility.EuclideanSobolev.sobolevToBounded line 62
  7. lemma OAI.TamingCompatibility.EuclideanSobolev.sobolevToBounded_spec line 70
  8. lemma OAI.TamingCompatibility.HilbertSobolev.boundedDistribution_schwartz line 89
  9. lemma OAI.TamingCompatibility.HilbertSobolev.sobolevToBounded_schwartz line 95
  10. lemma OAI.TamingCompatibility.HilbertSobolev.schwartz_sobolev_bound line 101
  11. lemma OAI.TamingCompatibility.HilbertSobolev.schwartzToH_derivative line 108
  12. lemma OAI.TamingCompatibility.HilbertSobolev.schwartz_second_derivative_bound line 114
  13. lemma OAI.TamingCompatibility.HilbertSobolev.schwartz_first_derivative_bound line 146
  14. lemma OAI.TamingCompatibility.HilbertSobolev.schwartz_two_jet_bound line 162