OAI/Probability/SKGap/Matrix/Word.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.SKGap.WordLetter line 14
2. def OAI.SKGap.WordLetter.bounded line 21
3. def OAI.SKGap.WordLetter.eval line 26
4. def OAI.SKGap.actualWord line 32
5. def OAI.SKGap.actualWordBound line 36
6. lemma OAI.SKGap.actualWordBound_pos line 39
7. lemma OAI.SKGap.WordLetter.eval_bounds line 45
8. theorem OAI.SKGap.actualWord_bounds line 76