OAI/Probability/SKGap/Matrix/WordLoop.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.wordDifferentialBound line 16
2. lemma OAI.SKGap.actualWord_elementary_bound line 19
3. def OAI.SKGap.actualWordLoop line 29
4. theorem OAI.SKGap.actualWord_loop line 34
5. lemma OAI.SKGap.wordPartners_lengths line 80
6. lemma OAI.SKGap.wordPartners_preserves_bound line 98
7. lemma OAI.SKGap.wordPartners_card_bound line 134
8. lemma OAI.SKGap.wordRecursionAt_lengths line 140
9. lemma OAI.SKGap.wordRecursionAt_bounds line 163
10. lemma OAI.SKGap.wordRecursionTerms_lengths line 177
11. lemma OAI.SKGap.wordRecursionTerms_bounds line 189
12. lemma OAI.SKGap.wordRecursionTerms_card_bound line 204