OAI/Probability/ThorpShuffle/WalshFlow.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thorp.Conditional.scatterPosition_eq_snoc line 16
2. theorem OAI.Thorp.Conditional.character_snoc line 24
3. theorem OAI.Thorp.Conditional.coefficient_physicalFlow_even line 29
4. theorem OAI.Thorp.Conditional.coefficient_physicalFlow_odd line 59
5. def OAI.Thorp.Conditional.oneFreeEnergy line 77
6. theorem OAI.Thorp.Conditional.mean_coefficient_physicalFlow_odd_sq line 83
7. def OAI.Thorp.Conditional.prefixZero line 97
8. instance OAI.Thorp.Conditional.prefixZeroDecidable line 100
9. theorem OAI.Thorp.Conditional.prefixZero_zero line 105
10. theorem OAI.Thorp.Conditional.prefixZero_full line 109
11. theorem OAI.Thorp.Conditional.prefixZero_cons line 120
12. theorem OAI.Thorp.Conditional.prefixZero_snoc line 134
13. theorem OAI.Thorp.Conditional.prefixZero_count line 144
14. def OAI.Thorp.Conditional.bandEnergy line 162
15. theorem OAI.Thorp.Conditional.bandEnergy_zero line 166
16. theorem OAI.Thorp.Conditional.bandEnergy_full line 178
17. theorem OAI.Thorp.Conditional.bandEnergy_cons line 183
18. theorem OAI.Thorp.Conditional.mean_indicator line 192
19. theorem OAI.Thorp.Conditional.mean_bandEnergy_physicalFlow line 196