OAI/Analysis/HardSphere/Cutoffs/DiameterTail.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.PathCutoff.free_diameterRatio_tail line 16
2. def OAI.HardSphere.PathCutoff.MeshRegular line 61
3. lemma OAI.HardSphere.PathCutoff.meshRegular_measurable line 65
4. lemma OAI.HardSphere.PathCutoff.capSum_eq_of_max line 76
5. lemma OAI.HardSphere.PathCutoff.mesh_irregular_sub line 86
6. lemma OAI.HardSphere.PathCutoff.free_mesh_regular_tail line 101
7. lemma OAI.HardSphere.PathCutoff.free_split_lintegral line 132
8. lemma OAI.HardSphere.PathCutoff.free_prefix_bound line 151
9. lemma OAI.HardSphere.PathCutoff.free_suffix_bound line 162
10. lemma OAI.HardSphere.PathCutoff.free_prefix_event line 174
11. lemma OAI.HardSphere.PathCutoff.free_suffix_event line 191