OAI/Analysis/HardSphere/Orbitals/Joint.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.CellOrbital.bump_separated line 20
2. lemma OAI.HardSphere.CellOrbital.cutoff_partials_disjoint line 39
3. def OAI.HardSphere.CellOrbital.joint line 50
4. lemma OAI.HardSphere.CellOrbital.joint_apply line 53
5. lemma OAI.HardSphere.CellOrbital.joint_real line 59
6. lemma OAI.HardSphere.CellOrbital.joint_partial line 64
7. lemma OAI.HardSphere.CellOrbital.joint_gradient_le line 71