OAI/Probability/ThorpShuffle/EnergyDecay.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thorp.Conditional.mean_rawFree_sweep line 14
2. theorem OAI.Thorp.Conditional.rawIterate_half_weight line 21
3. theorem OAI.Thorp.Conditional.rawIterate_half_free line 30
4. theorem OAI.Thorp.Conditional.mean_half_single line 39
5. theorem OAI.Thorp.Conditional.mean_half_factorization line 44
6. def OAI.Thorp.Conditional.rawEnergy line 62
7. def OAI.Thorp.Conditional.halfEnergy line 63
8. def OAI.Thorp.Conditional.partnerEnergy line 65
9. def OAI.Thorp.Conditional.startHalfDensity line 68
10. theorem OAI.Thorp.Conditional.halfEnergy_nonneg line 71
11. theorem OAI.Thorp.Conditional.rawEnergy_halves line 74
12. theorem OAI.Thorp.Conditional.oneFreeEnergy_partner line 81
13. theorem OAI.Thorp.Conditional.mean_half_energy_factorization line 91
14. theorem OAI.Thorp.Conditional.noise_bound_balanced_halves line 103
15. def OAI.Thorp.Conditional.splitHistory line 131
16. theorem OAI.Thorp.Conditional.mean_history_add line 144
17. theorem OAI.Thorp.Conditional.rawIterate_snoc line 151
18. theorem OAI.Thorp.Conditional.iterateState_snoc line 156
19. theorem OAI.Thorp.Conditional.rawIterate_append line 161
20. theorem OAI.Thorp.Conditional.iterateState_append line 172
21. theorem OAI.Thorp.Conditional.expectedEnergy_add line 183
22. theorem OAI.Thorp.Conditional.expectedNoise_add line 190