OAI/Analysis/HardSphere/Geometry/LocalCloseLabels.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.localCloseLabels line 25
  2. lemma OAI.HardSphere.localCloseSmoothCount_nonneg line 29
  3. lemma OAI.HardSphere.localCloseSmoothCount_covers line 32
  4. lemma OAI.HardSphere.closeAmplitude_ne_zero_imp line 46
  5. lemma OAI.HardSphere.closeAmplitude_mem_localized line 52
  6. lemma OAI.HardSphere.closeAmplitude_unique_site line 65
  7. theorem OAI.HardSphere.localCloseSmoothCount_sum_le line 77
  8. def OAI.HardSphere.configurationMollify line 112
  9. lemma OAI.HardSphere.configurationMollify_lift line 116
  10. lemma OAI.HardSphere.configurationMollify_integrable line 123
  11. lemma OAI.HardSphere.configurationMollify_smooth line 129
  12. lemma OAI.HardSphere.configurationMollify_nonneg line 137
  13. lemma OAI.HardSphere.configurationMollify_lipschitz line 142
  14. lemma OAI.HardSphere.configurationMollify_approximation line 160