OAI/Probability/DirectionalWalk/ShiftedBlocks.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalZeroOne.nthCommon_shift_prefix line 12
2. lemma OAI.DirectionalZeroOne.consecutiveThree_joins line 27
3. lemma OAI.DirectionalZeroOne.signedTotal_consecutiveThree line 45
4. lemma OAI.DirectionalZeroOne.consecutiveFour_total line 56
5. lemma OAI.DirectionalZeroOne.nthCommon_index_height line 70
6. lemma OAI.DirectionalZeroOne.listTotal_nthCommon line 76
7. lemma OAI.DirectionalZeroOne.departure_between_common line 82
8. lemma OAI.DirectionalZeroOne.commonBand_experiment_contact line 111
9. lemma OAI.DirectionalZeroOne.averageProd_left line 169
10. lemma OAI.DirectionalZeroOne.averageProd_right line 177
11. lemma OAI.DirectionalZeroOne.average_ge line 188
12. lemma OAI.DirectionalZeroOne.fourWindow_average line 199
13. lemma OAI.DirectionalZeroOne.fourWindow_ge line 211