OAI/Analysis/HardSphere/Geometry/MollifiedCloseCountMultiplier.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.mollifiedCloseCountMultiplier line 24
  2. lemma OAI.HardSphere.mollifiedCloseCountMultiplier_apply line 28
  3. lemma OAI.HardSphere.mollifiedCloseCountMultiplier_real line 32
  4. lemma OAI.HardSphere.mollifiedCloseCountMultiplier_gradient line 37
  5. def OAI.HardSphere.closeHighProfile line 48
  6. lemma OAI.HardSphere.closeHighProfile_smooth line 50
  7. lemma OAI.HardSphere.closeHighProfile_bounds line 53
  8. lemma OAI.HardSphere.closeHighProfile_zero line 58
  9. lemma OAI.HardSphere.closeHighProfile_one line 60
  10. lemma OAI.HardSphere.closeHighProfile_deriv line 63
  11. lemma OAI.HardSphere.closeHighProfile_deriv_zero line 66
  12. lemma OAI.HardSphere.closeHighProfile_deriv_bound line 70
  13. def OAI.HardSphere.mollifiedCloseCutoff line 76
  14. lemma OAI.HardSphere.mollifiedCloseCutoff_apply line 80
  15. lemma OAI.HardSphere.mollifiedCloseCutoff_partial line 86
  16. theorem OAI.HardSphere.mollifiedCloseCutoff_gradient line 94
  17. lemma OAI.HardSphere.euclideanProject_move_one_le line 125
  18. lemma OAI.HardSphere.localCloseRoot_away_eq line 138
  19. lemma OAI.HardSphere.mollifiedCloseRoot_away_eq line 146
  20. lemma OAI.HardSphere.mollifiedCloseCount_away_eq line 170