OAI/Analysis/HardSphere/Geometry/FreePathExpectation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.freePathExpectation line 20
2. lemma OAI.HardSphere.freePathExpectation_measurable line 24
3. lemma OAI.HardSphere.selected_start_integral line 29
4. lemma OAI.HardSphere.slice_mass_integral line 55
5. lemma OAI.HardSphere.selected_start_ground_integral line 88
6. lemma OAI.HardSphere.groundPathLaw_deletion line 96
7. def OAI.HardSphere.oneConfiguration line 163
8. def OAI.HardSphere.onePathAt line 165
9. lemma OAI.HardSphere.onePathAt_continuous line 168
10. lemma OAI.HardSphere.onePathAt_reverse line 174
11. lemma OAI.HardSphere.onePathAt_single line 177
12. lemma OAI.HardSphere.onePathAt_join_left line 183
13. lemma OAI.HardSphere.onePathAt_join_right line 189
14. def OAI.HardSphere.oneFreeExpectation line 195
15. lemma OAI.HardSphere.oneFreeExpectation_measurable line 198
16. lemma OAI.HardSphere.pathProduct_measurable line 202
17. lemma OAI.HardSphere.free_product_expectation line 207