OAI/Probability/DirectionalWalk/FreshPaths.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalZeroOne.freshPathKernel line 12
2. instance OAI.DirectionalZeroOne.(instance at line 15) line 15
3. def OAI.DirectionalZeroOne.freshJoint line 19
4. instance OAI.DirectionalZeroOne.(instance at line 23) line 23
5. lemma OAI.DirectionalZeroOne.freshJoint_apply line 28
6. lemma OAI.DirectionalZeroOne.freshJoint_path_marginal line 34
7. lemma OAI.DirectionalZeroOne.freshJoint_lintegral line 41
8. lemma OAI.DirectionalZeroOne.measurable_random_visitAfter line 48
9. def OAI.DirectionalZeroOne.quenchedReturn line 64
10. lemma OAI.DirectionalZeroOne.measurable_quenchedReturn line 68
11. def OAI.DirectionalZeroOne.returnAtLeast line 73
12. def OAI.DirectionalZeroOne.returnBin line 77
13. lemma OAI.DirectionalZeroOne.measurableSet_returnAtLeast line 81
14. lemma OAI.DirectionalZeroOne.measurableSet_returnBin line 86
15. lemma OAI.DirectionalZeroOne.freshJoint_return_visit_bound line 91
16. lemma OAI.DirectionalZeroOne.weighted_disjoint_measure_bound_ae line 100
17. lemma OAI.DirectionalZeroOne.weighted_contact_bin_bound_ae line 114