OAI/Probability/SKGap/Matrix/GOEDiagonalSquare.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.gaussian_goe_centered line 13
2. theorem OAI.SKGap.goe_diagonal_frobenius_tail line 21
3. def OAI.SKGap.removeDiagonal line 47
4. lemma OAI.SKGap.matrixWordSeminorm_le line 48
5. lemma OAI.SKGap.actualWord_removeDiagonal line 53
6. theorem OAI.SKGap.actual_word_simultaneous_zerodiag_of_cutoff line 73