OAI/Probability/SKGap/Matrix/WordBaseBias.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.wordDiagonal_nil line 15
2. lemma OAI.SKGap.wordDiagonal_diag line 17
3. lemma OAI.SKGap.wordDiagonal_noise line 20
4. lemma OAI.SKGap.wordDiagonal_inverse line 23
5. lemma OAI.SKGap.actualWord_all_diagonal line 26
6. lemma OAI.SKGap.actualWord_no_noise_entry line 46
7. lemma OAI.SKGap.wordDiagonal_bound line 73
8. def OAI.SKGap.wordExpected line 92
9. theorem OAI.SKGap.word_base_bias line 97
10. lemma OAI.SKGap.matrix_word_expectation_contraction line 123
11. theorem OAI.SKGap.goe_word_leading_contraction line 162