OAI/Probability/SKRatio/Matrices/RandomMatrixNet.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.MatrixNet.separated_card_le line 11
2. lemma OAI.SKRatio.MatrixNet.unit_ball_net line 42
3. lemma OAI.SKRatio.MatrixNet.opNorm_le_of_net line 83
4. lemma OAI.SKRatio.MatrixNet.opNorm_tail_of_bilinear line 118
5. lemma OAI.SKRatio.MatrixNet.matrix_opNorm_le_schur line 155
6. lemma OAI.SKRatio.MatrixNet.matrix_diagonal_opNorm_le line 191