OAI/Geometry/PrescribedPotential/SobolevLocalization.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Sobolev Localization.

  1. lemma OAI.SobolevChart.schwartz_deriv_product line 19
  2. lemma OAI.SobolevChart.weak_deriv_product line 35
  3. lemma OAI.SobolevChart.multiplier_add line 46
  4. lemma OAI.SobolevChart.bessel_two_laplacian line 52
  5. lemma OAI.SobolevChart.memSobolev_sum line 68
  6. lemma OAI.SobolevChart.memSobolev_of_laplacian line 79
  7. lemma OAI.SobolevChart.memSobolev_of_second_basis line 85
  8. lemma OAI.SobolevChart.memSobolev_zero_mul_schwartz line 93
  9. theorem OAI.SobolevChart.memSobolev_even_mul_schwartz line 103
  10. def OAI.SobolevChart.liftOperatorValue line 125
  11. lemma OAI.SobolevChart.realize_liftOperatorValue line 130
  12. def OAI.SobolevChart.liftOperatorLinear line 135
  13. lemma OAI.SobolevChart.realize_liftOperatorLinear line 146
  14. def OAI.SobolevChart.liftOperator line 152
  15. lemma OAI.SobolevChart.realize_liftOperator line 167
  16. def OAI.SobolevChart.cutoff line 174
  17. lemma OAI.SobolevChart.realize_cutoff line 178