OAI/Combinatorics/MatchingCount/Tapes/RandomWordLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.RandomWord.splitBits line 9
2. def OAI.MatchingFPRAS.RandomWord.gridBits line 12
3. def OAI.MatchingFPRAS.RandomWord.wordTapeEquiv line 14
4. lemma OAI.MatchingFPRAS.RandomWord.gridBits_apply line 18
5. lemma OAI.MatchingFPRAS.RandomWord.splitBits_symm line 20
6. lemma OAI.MatchingFPRAS.RandomWord.wordTape_list line 24
7. lemma OAI.MatchingFPRAS.RandomWord.wordTape_run line 46
8. theorem OAI.MatchingFPRAS.RandomWord.run_word line 55
9. def OAI.MatchingFPRAS.RandomWord.outputCoins line 61
10. def OAI.MatchingFPRAS.RandomWord.outputSplit line 64
11. lemma OAI.MatchingFPRAS.RandomWord.outputSplit_fst line 68
12. theorem OAI.MatchingFPRAS.RandomWord.outputCoins_fiber line 71