OAI/Probability/ThorpShuffle/Main.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thorp.full_mixing line 12
2. theorem OAI.Thorp.mixingTime_isBigO_orderFunction line 17
3. theorem OAI.Thorp.mixingTime_isTheta_orderFunction line 29
4. theorem OAI.Thorp.mixingTime_isTheta_log line 33
5. theorem OAI.Thorp.main line 41