OAI/Dynamics/ConditionalShuffle/Main.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.distance_antitone line 9
2. lemma OAI.Thorp.full_mixing_time line 18
3. lemma OAI.Thorp.full_mixing_constant line 25
4. lemma OAI.Thorp.support_lower_every_time line 29
5. lemma OAI.Revealed.twoHalfC_pos line 38
6. lemma OAI.Revealed.twoHalfC_lt_one line 46
7. lemma OAI.Revealed.twoHalfB_ge_four line 54
8. theorem OAI.Revealed.main line 60