OAI/Analysis/HardSphere/Cutoffs/RawAngleLift.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.TightCutoff.rawAngleLift line 20
2. def OAI.HardSphere.TightCutoff.rawCutoffReal line 23
3. lemma OAI.HardSphere.TightCutoff.rawAngleLift_smooth line 26
4. lemma OAI.HardSphere.TightCutoff.angle_project line 31
5. lemma OAI.HardSphere.TightCutoff.rawCutoffReal_smooth line 38
6. def OAI.HardSphere.TightCutoff.rawCutoff line 44
7. lemma OAI.HardSphere.TightCutoff.rawCutoff_real line 48
8. lemma OAI.HardSphere.TightCutoff.rawCutoff_norm_sq line 51
9. lemma OAI.HardSphere.TightCutoff.rawCutoff_clearance line 56
10. lemma OAI.HardSphere.TightCutoff.rawCutoffReal_bounds line 84
11. lemma OAI.HardSphere.TightCutoff.rawAngleLift_fderiv line 91
12. lemma OAI.HardSphere.TightCutoff.rawAngleLift_fderiv_coord line 110
13. lemma OAI.HardSphere.TightCutoff.rawCutoff_derivative_sq_le line 122
14. lemma OAI.HardSphere.TightCutoff.rawAngleLift_sum_squares line 142
15. lemma OAI.HardSphere.TightCutoff.pairQ_representative line 161
16. lemma OAI.HardSphere.TightCutoff.rawAngleLift_gradient_le line 169
17. lemma OAI.HardSphere.TightCutoff.rawCutoff_gradient_le line 192