OAI/Geometry/PrescribedPotential/CoreBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Core Bounds.

  1. def OAI.SobolevChart.CoreBound line 21
  2. lemma OAI.SobolevChart.CoreBound.comp line 24
  3. lemma OAI.SobolevChart.CoreBound.add line 31
  4. lemma OAI.SobolevChart.CoreBound.sum line 40
  5. lemma OAI.SobolevChart.CoreBound.id line 52
  6. lemma OAI.SobolevChart.coreBound_deriv line 61
  7. lemma OAI.SobolevChart.coreBound_word line 74
  8. lemma OAI.SobolevChart.schwartzCoord_distribution line 82
  9. lemma OAI.SobolevChart.schwartzCoord_raise_two line 86
  10. lemma OAI.SobolevChart.schwartzCoord_raise_two_norm line 101
  11. lemma OAI.SobolevChart.coreBound_raise_two line 117
  12. lemma OAI.SobolevChart.schwartzWord_append line 132
  13. lemma OAI.SobolevChart.coreBound_of_words line 140