OAI/Probability/DirectionalWalk/CommonBands.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalZeroOne.coveredDepthBand line 12
2. lemma OAI.DirectionalZeroOne.measurableSet_coveredDepthBand line 15
3. lemma OAI.DirectionalZeroOne.two_cuts_uncovered_mixed line 21
4. lemma OAI.DirectionalZeroOne.nthCommon_suffix_map line 57
5. def OAI.DirectionalZeroOne.consecutiveThree line 81
6. lemma OAI.DirectionalZeroOne.measurable_consecutiveThree line 86
7. lemma OAI.DirectionalZeroOne.consecutiveThree_law line 93
8. def OAI.DirectionalZeroOne.consecutiveFour line 115
9. lemma OAI.DirectionalZeroOne.measurable_consecutiveFour line 119
10. lemma OAI.DirectionalZeroOne.consecutiveFour_law line 125