OAI/Probability/ThorpShuffle/FiniteExpectation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thorp.Conditional.mean_congr line 16
2. theorem OAI.Thorp.Conditional.mean_zero line 22
3. theorem OAI.Thorp.Conditional.mean_const line 25
4. theorem OAI.Thorp.Conditional.mean_add line 30
5. theorem OAI.Thorp.Conditional.mean_mul_const line 34
6. theorem OAI.Thorp.Conditional.mean_const_mul line 39
7. theorem OAI.Thorp.Conditional.mean_sum line 43
8. theorem OAI.Thorp.Conditional.mean_nonneg line 48
9. theorem OAI.Thorp.Conditional.mean_le_mean line 52
10. theorem OAI.Thorp.Conditional.mean_le_const line 56
11. theorem OAI.Thorp.Conditional.mean_equiv line 60
12. theorem OAI.Thorp.Conditional.mean_prod line 67
13. theorem OAI.Thorp.Conditional.mean_comm line 73
14. theorem OAI.Thorp.Conditional.mean_history_succ line 79
15. theorem OAI.Thorp.run_zero line 88
16. theorem OAI.Thorp.run_succ line 91
17. theorem OAI.Thorp.Conditional.iterateState_free line 99
18. theorem OAI.Thorp.Conditional.iterateState_freeCount line 110
19. theorem OAI.Thorp.Conditional.expectedEnergy_succ line 117