OAI/Analysis/HardSphere/Geometry/HeadLift.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.headLift line 20
  2. lemma OAI.HardSphere.headLift_direction_zero line 23
  3. lemma OAI.HardSphere.headLift_direction_succ line 30
  4. def OAI.HardSphere.SmoothMultiplier.orbital line 35
  5. lemma OAI.HardSphere.SmoothMultiplier.orbital_continuous line 38
  6. def OAI.HardSphere.SmoothMultiplier.orbitalBound line 42
  7. lemma OAI.HardSphere.SmoothMultiplier.orbital_le_bound line 45
  8. def OAI.HardSphere.SmoothMultiplier.orbitalEnergy line 49
  9. def OAI.HardSphere.SmoothMultiplier.liftHead line 52
  10. lemma OAI.HardSphere.SmoothMultiplier.coordDerivative_liftHead_zero line 56
  11. lemma OAI.HardSphere.SmoothMultiplier.coordDerivative_liftHead_succ line 69
  12. lemma OAI.HardSphere.SmoothMultiplier.liftHead_gradient_sum line 80