OAI/Analysis/HardSphere/Geometry/AddedSites.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Lattice.addedSites line 10
2. lemma OAI.HardSphere.Lattice.torus_unit_offsets_card line 13
3. lemma OAI.HardSphere.Lattice.addedSites_card line 17
4. lemma OAI.HardSphere.Lattice.mem_addedSites line 26
5. def OAI.HardSphere.Lattice.encounterSet line 49
6. lemma OAI.HardSphere.Lattice.mem_encounterSet line 53
7. lemma OAI.HardSphere.Lattice.encounterSet_card_le line 58
8. lemma OAI.HardSphere.Lattice.encounterSet_card_le_right line 75
9. theorem OAI.HardSphere.Lattice.encounter_charge_bound line 84
10. def OAI.HardSphere.Lattice.torusContact line 124
11. def OAI.HardSphere.Lattice.shellAttachment line 127
12. lemma OAI.HardSphere.Lattice.near_badComponent_eq line 132
13. lemma OAI.HardSphere.Lattice.shell_encounter_charge line 140
14. theorem OAI.HardSphere.Lattice.torus_detour_charge line 161