OAI/Probability/ThorpShuffle/FreshCoins.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thorp.Conditional.expectedBand line 16
2. def OAI.Thorp.Conditional.expectedNoise line 20
3. theorem OAI.Thorp.Conditional.mean_div_const line 24
4. theorem OAI.Thorp.Conditional.expectedBand_zero line 28
5. theorem OAI.Thorp.Conditional.expectedBand_full line 36
6. theorem OAI.Thorp.Conditional.two_pow_ratio line 46
7. theorem OAI.Thorp.Conditional.expectedBand_succ line 51
8. theorem OAI.Thorp.Conditional.expectedEnergy_recurrence line 71
9. theorem OAI.Thorp.Conditional.mean_product_bits line 83
10. def OAI.Thorp.Conditional.pairFreeCount line 93
11. def OAI.Thorp.Conditional.pairHalfCount line 96
12. theorem OAI.Thorp.Conditional.local_balance_factor line 100
13. theorem OAI.Thorp.Conditional.balance_exponential_mean line 106
14. theorem OAI.Thorp.Conditional.pair_half_balance line 133
15. theorem OAI.Thorp.Conditional.pair_both_half_balance line 150