OAI/Geometry/PrescribedPotential/SobolevProduct.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Sobolev Product.

  1. lemma OAI.SobolevChart.boundedDistribution_schwartz line 20
  2. lemma OAI.SobolevChart.strongEmbedding_schwartz line 26
  3. lemma OAI.SobolevChart.schwartz_word_sup_bound line 31
  4. def OAI.SobolevChart.BinaryCoreBound line 44
  5. lemma OAI.SobolevChart.BinaryCoreBound.add line 48
  6. lemma OAI.SobolevChart.binaryBound_raise_one line 57
  7. lemma OAI.SobolevChart.binaryBound_of_words line 93
  8. lemma OAI.SobolevChart.schwartz_product_swap line 112
  9. lemma OAI.SobolevChart.binaryBound_product_words_zero line 118
  10. lemma OAI.SobolevChart.binaryBound_word_product line 147
  11. theorem OAI.SobolevChart.schwartz_sobolev_product_bound line 163