OAI/Combinatorics/MatchingCount/Tapes/OnlineWord.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.OnlineWord.prepend line 9
2. lemma OAI.MatchingFPRAS.OnlineWord.mean_prepend line 12
3. def OAI.MatchingFPRAS.OnlineWord.reverseBits line 21
4. lemma OAI.MatchingFPRAS.OnlineWord.ofFn_reverse line 26
5. lemma OAI.MatchingFPRAS.OnlineWord.average_reverse line 37
6. lemma OAI.MatchingFPRAS.OnlineWord.mean_prepend_nil line 42
7. def OAI.MatchingFPRAS.OnlineWord.step line 48
8. def OAI.MatchingFPRAS.OnlineWord.stepRealizer line 49
9. lemma OAI.MatchingFPRAS.OnlineWord.fold_step line 54
10. def OAI.MatchingFPRAS.OnlineWord.listRealizer line 60
11. def OAI.MatchingFPRAS.OnlineWord.naturalRealizer line 68
12. lemma OAI.MatchingFPRAS.OnlineWord.all_length line 72