OAI/Analysis/HardSphere/Geometry/MollifiedCloseJoint.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.mollifiedCloseCutoff_partials_disjoint line 32
  2. def OAI.HardSphere.mollifiedCloseJoint line 46
  3. lemma OAI.HardSphere.mollifiedCloseJoint_apply line 51
  4. lemma OAI.HardSphere.mollifiedCloseJoint_real line 57
  5. lemma OAI.HardSphere.mollifiedCloseJoint_partial line 62
  6. theorem OAI.HardSphere.mollifiedCloseJoint_gradient line 71
  7. lemma OAI.HardSphere.closeCount_mollified_comparison line 108
  8. lemma OAI.HardSphere.mollifiedCloseCutoff_nonzero_count line 128
  9. lemma OAI.HardSphere.mollifiedCloseCutoff_covers line 141
  10. lemma OAI.HardSphere.mollifiedCloseJoint_covers line 151
  11. lemma OAI.HardSphere.mollifiedCloseJoint_nonzero_count line 159
  12. lemma OAI.HardSphere.exists_close_mollifier line 173