OAI/Probability/SKGap/Matrix/GOESparse.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.principalOperatorNorm line 14
2. lemma OAI.SKGap.principalOperatorNorm_empty line 18
3. lemma OAI.SKGap.goe_sparse_one_tail line 24
4. theorem OAI.SKGap.goe_sparse_union_tail line 58
5. lemma OAI.SKGap.supported_quad_eq line 91
6. lemma OAI.SKGap.supported_norm_sq_eq line 111
7. lemma OAI.SKGap.supported_quad_le_principal line 119