OAI/Probability/ThorpShuffle/MixingBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thorp.exists_mixing_time_succ line 12
2. theorem OAI.Thorp.exists_mixing_time line 48
3. theorem OAI.Thorp.exact_support_lower line 52
4. theorem OAI.Thorp.log_factorial_lower line 56
5. theorem OAI.Thorp.supportThreshold_bounds line 65
6. theorem OAI.Thorp.supportThreshold_isBigO line 129
7. theorem OAI.Thorp.orderFunction_isBigO_mixingTime line 139