OAI/Probability/SKGap/Matrix/GOESubmatrix.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.coordinates_restrict_hasLaw line 15
2. def OAI.SKGap.matrixCoordinatesEmbedding line 20
3. lemma OAI.SKGap.goeMatrix_submatrix line 24
4. lemma OAI.SKGap.continuous_matrixOperator line 27
5. lemma OAI.SKGap.continuous_goeMatrix line 35
6. lemma OAI.SKGap.goe_restricted_norm_tail line 39
7. lemma OAI.SKGap.matrix_quad_row_bound line 69
8. lemma OAI.SKGap.matrixOperator_norm_le_row line 99
9. lemma OAI.SKGap.matrixOperator_eq_toEuclideanCLM line 110
10. lemma OAI.SKGap.goe_diagonal_hasLaw line 125
11. lemma OAI.SKGap.goe_diagonal_tail line 135
12. lemma OAI.SKGap.diagonal_norm_le line 154