OAI/Analysis/HardSphere/Geometry/SimplePath.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HardSphere.Lattice.SimplePath line 15
2. instance OAI.HardSphere.Lattice.simplePathMeasurableSpace line 18
3. instance OAI.HardSphere.Lattice.simplePathCountable line 21
4. instance OAI.HardSphere.Lattice.environmentMeasurableSpace line 26
5. def OAI.HardSphere.Lattice.forgetGood line 28
6. def OAI.HardSphere.Lattice.simpleEncounter line 31
7. def OAI.HardSphere.Lattice.simplePathGood line 34
8. lemma OAI.HardSphere.Lattice.pmf_lintegral_discrete line 37
9. lemma OAI.HardSphere.Lattice.pmf_event_discrete line 45
10. lemma OAI.HardSphere.Lattice.forgetGood_full_mass line 53
11. lemma OAI.HardSphere.Lattice.forgetGood_double_moment line 61
12. lemma OAI.HardSphere.Lattice.mapped_bad_law line 68
13. lemma OAI.HardSphere.Lattice.finite_datum_expectation line 80
14. theorem OAI.HardSphere.Lattice.good_paths_measurable line 89