OAI/Analysis/HardSphere/Cutoffs/ThreeTorus.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PeriodicCutoff.ThreeTorus line 19
  2. def OAI.PeriodicCutoff.box line 21
  3. lemma OAI.PeriodicCutoff.box_measurable line 25
  4. lemma OAI.PeriodicCutoff.box_volume_le line 28
  5. def OAI.PeriodicCutoff.pairQ line 38
  6. def OAI.PeriodicCutoff.qLift line 40
  7. lemma OAI.PeriodicCutoff.pairQ_continuous line 42
  8. lemma OAI.PeriodicCutoff.pairQ_coe line 48
  9. lemma OAI.PeriodicCutoff.pairQ_nonneg line 58
  10. lemma OAI.PeriodicCutoff.pairQ_le line 61
  11. lemma OAI.PeriodicCutoff.not_mem_box_pairQ line 66
  12. def OAI.PeriodicCutoff.angle line 79
  13. def OAI.PeriodicCutoff.angleLift line 82
  14. lemma OAI.PeriodicCutoff.angleLift_smooth line 86
  15. lemma OAI.PeriodicCutoff.angle_bounds line 94
  16. lemma OAI.PeriodicCutoff.angle_zero line 100
  17. lemma OAI.PeriodicCutoff.angle_one line 105
  18. lemma OAI.PeriodicCutoff.angle_one_outside line 110
  19. def OAI.PeriodicCutoff.angleFactor line 114
  20. def OAI.PeriodicCutoff.anglePartial line 117
  21. lemma OAI.PeriodicCutoff.angleLift_derivative line 121
  22. lemma OAI.PeriodicCutoff.qLift_nonneg line 137
  23. lemma OAI.PeriodicCutoff.chordLift_le_qLift line 141
  24. lemma OAI.PeriodicCutoff.angleFactor_eq_zero line 145
  25. lemma OAI.PeriodicCutoff.anglePartial_eq_zero line 156
  26. lemma OAI.PeriodicCutoff.anglePartial_sq_le line 160