OAI/Geometry/PrescribedPotential/SobolevEmbedding.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Sobolev Embedding.

  1. def OAI.SobolevChart.inverseWeight line 18
  2. lemma OAI.SobolevChart.inverseWeight_temperate line 31
  3. lemma OAI.SobolevChart.weight_cancel line 36
  4. lemma OAI.SobolevChart.all_even_bessel_fourier_L1 line 45
  5. lemma OAI.SobolevChart.all_even_fourier_moments line 57
  6. def OAI.SobolevChart.boundedDistribution line 102
  7. lemma OAI.SobolevChart.boundedDistribution_apply line 105
  8. lemma OAI.SobolevChart.fourier_L1_distribution line 112
  9. lemma OAI.SobolevChart.fourierInv_L1_distribution line 122
  10. lemma OAI.SobolevChart.fourier_temperate_of_moments line 133
  11. theorem OAI.SobolevChart.all_even_smooth_representative line 145