OAI/Analysis/HardSphere/Geometry/SmallComponent.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.BathSlice.SmallComponent line 14
2. lemma OAI.HardSphere.BathSlice.small_fill_coordinate line 17
3. def OAI.HardSphere.BathSlice.microColumn line 36
4. lemma OAI.HardSphere.BathSlice.small_fill_subset_columns line 41
5. lemma OAI.HardSphere.BathSlice.volume_microColumn_le line 70
6. lemma OAI.HardSphere.BathSlice.microColumn_eq_of_projection line 91
7. def OAI.HardSphere.BathSlice.bathWitnessCover line 111
8. lemma OAI.HardSphere.BathSlice.card_bathWitnessCover_le line 115
9. lemma OAI.HardSphere.BathSlice.bad_has_bathWitness line 122
10. def OAI.HardSphere.BathSlice.smallFills line 132
11. theorem OAI.HardSphere.BathSlice.volume_smallFills_le line 135