OAI/Analysis/HardSphere/Geometry/AnimalFamily.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Lattice.animalFamily line 18
2. lemma OAI.HardSphere.Lattice.animalFamily_card_le line 21
3. lemma OAI.HardSphere.Lattice.mem_animalFamily_card line 29
4. def OAI.HardSphere.Lattice.LargeBadComponent line 34
5. lemma OAI.HardSphere.Lattice.largeBadComponent_contains_animal line 37
6. theorem OAI.HardSphere.Lattice.largeBadComponent_probability line 48
7. def OAI.HardSphere.BathSlice.parent line 86
8. def OAI.HardSphere.BathSlice.coarseCenter line 88
9. lemma OAI.HardSphere.BathSlice.gridCorner_dist_parent line 91
10. lemma OAI.HardSphere.BathSlice.witnesses_pairClose line 109
11. lemma OAI.HardSphere.BathSlice.pairClose_card_mono line 126
12. theorem OAI.HardSphere.BathSlice.large_component_forces_close line 138