OAI/Geometry/PrescribedPotential/SobolevParametrix.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Sobolev Parametrix.

  1. abbrev OAI.SobolevChart.L2 line 20
  2. def OAI.SobolevChart.realize line 24
  3. lemma OAI.SobolevChart.bessel_realize line 27
  4. lemma OAI.SobolevChart.realize_memSobolev line 31
  5. lemma OAI.SobolevChart.l2_injective line 34
  6. lemma OAI.SobolevChart.realize_injective line 37
  7. lemma OAI.SobolevChart.memSobolev_iff_realize line 43
  8. def OAI.SobolevChart.multiply line 54
  9. lemma OAI.SobolevChart.multiply_eq line 57
  10. lemma OAI.SobolevChart.multiply_norm_le line 65
  11. lemma OAI.SobolevChart.multiply_distribution line 75
  12. def OAI.SobolevChart.multiplier line 82
  13. lemma OAI.SobolevChart.multiplier_norm_le line 85
  14. lemma OAI.SobolevChart.multiplier_distribution line 91
  15. lemma OAI.SobolevChart.bessel_multiplier_comm line 99
  16. lemma OAI.SobolevChart.realize_multiplier line 106
  17. def OAI.FrozenPoisson.gainSymbol line 119
  18. lemma OAI.FrozenPoisson.gainSymbol_temperate line 122
  19. def OAI.FrozenPoisson.ellipticBound line 129
  20. lemma OAI.FrozenPoisson.ellipticBound_pos line 132
  21. lemma OAI.FrozenPoisson.gainSymbol_bound line 135
  22. def OAI.FrozenPoisson.gainSymbolBCF line 139
  23. lemma OAI.FrozenPoisson.gainSymbolBCF_norm line 143
  24. def OAI.FrozenPoisson.hilbertResolvent line 148
  25. lemma OAI.FrozenPoisson.hilbertResolvent_bound line 151
  26. lemma OAI.FrozenPoisson.bessel_two_resolvent line 157
  27. lemma OAI.FrozenPoisson.hilbertResolvent_realize line 168
  28. theorem OAI.FrozenPoisson.hilbert_frozen_inverse line 184