OAI/Analysis/HardSphere/Geometry/BoxWeight.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.BathSlice.boxWeight line 16
2. lemma OAI.HardSphere.BathSlice.volume_largeBoxUnion_le line 18
3. lemma OAI.HardSphere.BathSlice.pairCloseLabels_measurable line 40
4. lemma OAI.HardSphere.BathSlice.measurable_closeSet line 66
5. lemma OAI.HardSphere.BathSlice.volume_torus line 75
6. lemma OAI.HardSphere.BathSlice.microperiod_length line 80
7. theorem OAI.HardSphere.BathSlice.omitted_volume_le line 86
8. theorem OAI.HardSphere.BathSlice.omitted_mean_marginal line 120
9. lemma OAI.HardSphere.BathSlice.boxWeight_le line 133
10. lemma OAI.HardSphere.BathSlice.box_series_le line 146
11. theorem OAI.HardSphere.BathSlice.omitted_mean_le line 159