OAI/Probability/SKGap/Localization/BilinearCoefficient.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.RandomMatrix.gaussian_linear_upper_tail line 34
2. lemma OAI.SKGapCutoff.RandomMatrix.gaussian_linear_abs_tail line 59
3. def OAI.SKGapCutoff.RandomMatrix.bilinearCoefficient line 76
4. lemma OAI.SKGapCutoff.RandomMatrix.bilinear_sampled line 79
5. lemma OAI.SKGapCutoff.RandomMatrix.bilinearCoefficient_sq_le line 102
6. lemma OAI.SKGapCutoff.RandomMatrix.sampled_inner line 129
7. lemma OAI.SKGapCutoff.RandomMatrix.sampled_inner_tail line 137
8. lemma OAI.SKGapCutoff.RandomMatrix.sampled_opNorm_tail line 160
9. lemma OAI.SKGapCutoff.RandomMatrix.sampled_opNorm_tendsto line 201
10. lemma OAI.SKGapCutoff.RandomMatrix.gaussian_entry_tail line 230
11. lemma OAI.SKGapCutoff.RandomMatrix.sampled_maxEntry_tail line 254
12. lemma OAI.SKGapCutoff.RandomMatrix.sampled_maxEntry_tendsto line 278
13. lemma OAI.SKGapCutoff.RandomMatrix.matrix_column_sq_le line 298
14. lemma OAI.SKGapCutoff.RandomMatrix.matrix_bilinear_le line 315
15. lemma OAI.SKGapCutoff.RandomMatrix.matrix_entry_le_opNorm line 343
16. lemma OAI.SKGapCutoff.RandomMatrix.rough_square_of_opNorm line 350
17. lemma OAI.SKGapCutoff.RandomMatrix.sampled_rough_square_good line 364