OAI/Analysis/HardSphere/Geometry/BadComponent.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Lattice.isBadComponent_iff line 17
2. lemma OAI.HardSphere.Lattice.finiteBadComponents_iff line 37
3. lemma OAI.HardSphere.BathSlice.measurable_component_test line 56
4. lemma OAI.HardSphere.BathSlice.measurable_finiteComponents_test line 74
5. lemma OAI.HardSphere.BathSlice.measurable_exceptional line 83
6. theorem OAI.HardSphere.BathSlice.measurableSet_omitted_graph line 88
7. lemma OAI.HardSphere.BathSlice.measurableSet_omitted line 102
8. lemma OAI.HardSphere.BathSlice.measurableSet_retained line 108
9. theorem OAI.HardSphere.BathSlice.measurable_omitted_volume line 111
10. theorem OAI.HardSphere.Lattice.fill_column_meets line 119
11. def OAI.HardSphere.Lattice.columnCover line 130
12. lemma OAI.HardSphere.Lattice.fill_subset_columnCover line 133
13. lemma OAI.HardSphere.Lattice.card_columnCover_le line 148
14. lemma OAI.HardSphere.Lattice.finite_fill line 157
15. theorem OAI.HardSphere.Lattice.ncard_fill_le_columns line 176