OAI/Probability/DirectionalWalk/SumLaws.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalZeroOne.sumLaw line 16
2. instance OAI.DirectionalZeroOne.conv_probability line 20
3. instance OAI.DirectionalZeroOne.sumLaw_probability line 24
4. lemma OAI.DirectionalZeroOne.sumLaw_add line 32
5. lemma OAI.DirectionalZeroOne.entropy_conv_ge_left line 39
6. lemma OAI.DirectionalZeroOne.sumLaw_entropy_monotone line 61
7. lemma OAI.DirectionalZeroOne.sumLaw_lattice_moment line 73
8. lemma OAI.DirectionalZeroOne.sumLaw_lattice_entropy line 107
9. def OAI.DirectionalZeroOne.listTotal line 125
10. def OAI.DirectionalZeroOne.pairTotal line 126
11. lemma OAI.DirectionalZeroOne.listTotal_prefix line 129
12. lemma OAI.DirectionalZeroOne.commonCutIndices_add line 133
13. lemma OAI.DirectionalZeroOne.listTotal_commonCut_add line 147
14. lemma OAI.DirectionalZeroOne.nthCommonList_total line 159
15. lemma OAI.DirectionalZeroOne.nthCommonList_pairTotal line 179
16. lemma OAI.DirectionalZeroOne.iid_sum_law line 189
17. def OAI.DirectionalZeroOne.commonGapLaw line 210
18. instance OAI.DirectionalZeroOne.commonBlockLaw_probability line 214
19. instance OAI.DirectionalZeroOne.commonGapLaw_probability line 218
20. lemma OAI.DirectionalZeroOne.nthCommonLaw_pairTotal line 222