OAI/Analysis/HardSphere/Geometry/TestVector.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.testVector line 22
  2. lemma OAI.HardSphere.testVector_smooth line 25
  3. lemma OAI.HardSphere.testVector_continuous line 29
  4. lemma OAI.HardSphere.testVector_derivative line 32
  5. def OAI.HardSphere.rmsTestFun line 40
  6. lemma OAI.HardSphere.rmsTest_smooth line 43
  7. lemma OAI.HardSphere.rmsTest_support line 47
  8. def OAI.HardSphere.SmoothTest.rms line 62
  9. lemma OAI.HardSphere.rmsTest_derivative_le line 72
  10. lemma OAI.HardSphere.rmsTest_energy_le line 93
  11. lemma OAI.HardSphere.rmsTest_norm_limit line 111