OAI/Probability/ThorpShuffle/EightBlocks.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.law_complexSign_zero line 13
2. def OAI.Thorp.Block.fullRate line 24
3. lemma OAI.Thorp.Block.exceptional_cube_tendsto line 28
4. lemma OAI.Thorp.Block.fullRate_tendsto line 33
5. lemma OAI.Thorp.Block.reciprocal_atMost_three line 42
6. lemma OAI.Thorp.Block.distance_eight_eventually line 54
7. lemma OAI.Thorp.Block.full_mixing_shift line 88