OAI/Analysis/HardSphere/Cutoffs/Near.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.TightCutoff.near line 27
  2. lemma OAI.HardSphere.TightCutoff.near_measurable line 30
  3. lemma OAI.HardSphere.TightCutoff.distance_sum_le_pairQ line 33
  4. lemma OAI.HardSphere.TightCutoff.near_distance_sum line 38
  5. lemma OAI.HardSphere.TightCutoff.near_subset_box line 46
  6. lemma OAI.HardSphere.TightCutoff.near_volume_le line 55
  7. lemma OAI.HardSphere.TightCutoff.near_distance line 62
  8. def OAI.HardSphere.TightCutoff.angle line 75
  9. def OAI.HardSphere.TightCutoff.angleLift line 78
  10. lemma OAI.HardSphere.TightCutoff.angleLift_smooth line 82
  11. lemma OAI.HardSphere.TightCutoff.angle_bounds line 90
  12. lemma OAI.HardSphere.TightCutoff.angle_zero line 96
  13. lemma OAI.HardSphere.TightCutoff.angle_one line 101
  14. lemma OAI.HardSphere.TightCutoff.angle_one_outside line 106
  15. def OAI.HardSphere.TightCutoff.angleFactor line 116
  16. def OAI.HardSphere.TightCutoff.anglePartial line 119
  17. lemma OAI.HardSphere.TightCutoff.angleLift_derivative line 123
  18. lemma OAI.HardSphere.TightCutoff.angleFactor_eq_zero line 139
  19. lemma OAI.HardSphere.TightCutoff.anglePartial_eq_zero line 150
  20. lemma OAI.HardSphere.TightCutoff.anglePartial_sq_le line 154