OAI/Geometry/TamingCompatibility/Functional/SobolevSpace.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TamingCompatibility.HilbertSobolev.H line 16
  2. def OAI.TamingCompatibility.HilbertSobolev.toDistribution line 18
  3. lemma OAI.TamingCompatibility.HilbertSobolev.lp_injective line 23
  4. lemma OAI.TamingCompatibility.HilbertSobolev.toDistribution_injective line 27
  5. lemma OAI.TamingCompatibility.HilbertSobolev.bessel_toDistribution line 35
  6. lemma OAI.TamingCompatibility.HilbertSobolev.toDistribution_memSobolev line 41
  7. theorem OAI.TamingCompatibility.HilbertSobolev.range_toDistribution line 45
  8. def OAI.TamingCompatibility.HilbertSobolev.multiplyLp line 57
  9. lemma OAI.TamingCompatibility.HilbertSobolev.multiplyLp_norm_le line 66
  10. def OAI.TamingCompatibility.HilbertSobolev.boundedFourierMultiplier line 70
  11. lemma OAI.TamingCompatibility.HilbertSobolev.boundedFourierMultiplier_apply line 75
  12. lemma OAI.TamingCompatibility.HilbertSobolev.boundedFourierMultiplier_norm_le line 79
  13. lemma OAI.TamingCompatibility.HilbertSobolev.toLp_top_norm_le line 86
  14. lemma OAI.TamingCompatibility.HilbertSobolev.boundedFourierMultiplier_distribution line 95
  15. lemma OAI.TamingCompatibility.HilbertSobolev.bessel_fourierMultiplier_comm line 106
  16. lemma OAI.TamingCompatibility.HilbertSobolev.toDistribution_boundedFourierMultiplier line 114
  17. def OAI.TamingCompatibility.HilbertSobolev.reindex line 125
  18. lemma OAI.TamingCompatibility.HilbertSobolev.toDistribution_reindex line 127
  19. def OAI.TamingCompatibility.HilbertSobolev.weight line 134
  20. lemma OAI.TamingCompatibility.HilbertSobolev.weight_temperate line 137
  21. lemma OAI.TamingCompatibility.HilbertSobolev.weight_le_one line 142
  22. lemma OAI.TamingCompatibility.HilbertSobolev.weight_memLp_top line 146
  23. def OAI.TamingCompatibility.HilbertSobolev.inclusion line 151
  24. lemma OAI.TamingCompatibility.HilbertSobolev.inclusion_norm_le line 155
  25. lemma OAI.TamingCompatibility.HilbertSobolev.toDistribution_inclusion line 164
  26. lemma OAI.TamingCompatibility.HilbertSobolev.inclusion_injective line 176