OAI/Probability/SKGap/Localization/Bilinear.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.operator_le_frobenius line 16
2. def OAI.SKGap.matrixBilinear line 24
3. lemma OAI.SKGap.matrixBilinear_inner line 27
4. lemma OAI.SKGap.matrixBilinear_abs_le line 37
5. lemma OAI.SKGap.matrixBilinear_frobenius line 46
6. lemma OAI.SKGap.matrixBilinear_sub line 52
7. lemma OAI.SKGap.matrixBilinear_integral line 57
8. lemma OAI.SKGap.matrixBilinear_diagonal_error line 70
9. lemma OAI.SKGap.goe_bilinear_lipschitz line 76
10. lemma OAI.SKGap.gaussianProduct_tail_lipschitz line 101
11. lemma OAI.SKGap.goe_entries_integrable line 134
12. lemma OAI.SKGap.goe_bilinear_bias line 146
13. lemma OAI.SKGap.gaussianProduct_tail_from_bias line 170
14. lemma OAI.SKGap.goe_bilinear_uniform_lipschitz line 186
15. lemma OAI.SKGap.goe_bilinear_concentration line 198