OAI/Probability/SKGap/Gaussian/MatrixNormTail.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.matrixWordSeminorm line 14
2. lemma OAI.SKGap.matrixWordSeminorm_lipschitz line 16
3. lemma OAI.SKGap.matrixWordSeminorm_add line 20
4. lemma OAI.SKGap.matrixWordSeminorm_nonneg line 25
5. lemma OAI.SKGap.matrixCentered_sub line 31
6. lemma OAI.SKGap.gaussianProduct_centered_matrix_tail line 41
7. lemma OAI.SKGap.gaussianMatrix_scaled_semnorm_tail line 78