OAI/Analysis/HardSphere/Geometry/RawAngleLift.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.rawAngleLift line 22
  2. def OAI.HardSphere.rawCutoffReal line 25
  3. lemma OAI.HardSphere.rawAngleLift_smooth line 28
  4. lemma OAI.HardSphere.angle_project line 33
  5. lemma OAI.HardSphere.rawCutoffReal_smooth line 40
  6. def OAI.HardSphere.rawCutoff line 46
  7. lemma OAI.HardSphere.rawCutoff_real line 50
  8. lemma OAI.HardSphere.rawCutoff_norm_sq line 53
  9. lemma OAI.HardSphere.rawCutoff_clearance line 58
  10. lemma OAI.HardSphere.torus_volume_real line 87
  11. lemma OAI.HardSphere.rawCutoffReal_bounds line 92
  12. lemma OAI.HardSphere.rawCutoff_mass_pointwise line 99
  13. lemma OAI.HardSphere.rawCutoff_mass_lower line 119
  14. lemma OAI.HardSphere.rawAngleLift_fderiv line 147
  15. lemma OAI.HardSphere.rawAngleLift_fderiv_coord line 166
  16. lemma OAI.HardSphere.rawCutoff_derivative_sq_le line 178