OAI/Probability/SKRatio/Matrices/GaussianSquareMatrix.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.MatrixNet.independent_sum_upper_tail line 16
2. lemma OAI.SKRatio.MatrixNet.gaussian_squareTail_row_bound line 41
3. def OAI.SKRatio.MatrixNet.incidentEdges line 94
4. lemma OAI.SKRatio.MatrixNet.incidentEdges_card_le line 97
5. lemma OAI.SKRatio.MatrixNet.sum_coupling_row line 113
6. lemma OAI.SKRatio.MatrixNet.abs_coupling line 123
7. lemma OAI.SKRatio.MatrixNet.coupling_nonneg line 128
8. lemma OAI.SKRatio.MatrixNet.coupling_add line 133
9. lemma OAI.SKRatio.MatrixNet.coupling_sub line 140
10. lemma OAI.SKRatio.MatrixNet.coupling_const_mul line 147
11. lemma OAI.SKRatio.MatrixNet.coupling_const_norm_le line 154
12. lemma OAI.SKRatio.MatrixNet.integrable_standard_square line 164
13. lemma OAI.SKRatio.MatrixNet.standard_square_integral line 167
14. def OAI.SKRatio.MatrixNet.clippedSquare line 172
15. lemma OAI.SKRatio.MatrixNet.continuous_clippedSquare line 174
16. lemma OAI.SKRatio.MatrixNet.clippedSquare_nonneg line 177
17. lemma OAI.SKRatio.MatrixNet.clippedSquare_le line 179
18. lemma OAI.SKRatio.MatrixNet.square_sub_clip_nonneg line 181
19. lemma OAI.SKRatio.MatrixNet.square_sub_clip_le line 184
20. lemma OAI.SKRatio.MatrixNet.clippedSquare_integrable line 193
21. lemma OAI.SKRatio.MatrixNet.clippedSquare_mean_bounds line 198
22. lemma OAI.SKRatio.MatrixNet.clippedSquare_mean_error line 206
23. lemma OAI.SKRatio.MatrixNet.centered_clip_subgaussian line 223
24. lemma OAI.SKRatio.MatrixNet.clipped_square_matrix_rare line 242
25. lemma OAI.SKRatio.MatrixNet.square_remainder_norm_le line 261
26. lemma OAI.SKRatio.MatrixNet.coupling_norm_add_three line 278
27. lemma OAI.SKRatio.MatrixNet.centered_square_mean_norm_le line 289
28. lemma OAI.SKRatio.MatrixNet.centered_square_norm_le line 302
29. theorem OAI.SKRatio.MatrixNet.centered_gaussian_square_matrix_rare line 323