OAI/Probability/SKGap/Brownian/PathDiagonal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.pathDiagonal line 63
2. def OAI.SKGap.pathShift line 65
3. lemma OAI.SKGap.stabilityMatrix_path_rep line 67
4. lemma OAI.SKGap.pathDiagonal_opNorm line 85
5. lemma OAI.SKGap.pathShift_opNorm line 94
6. lemma OAI.SKGap.stabilityMatrix_opNorm line 101
7. lemma OAI.SKGap.diagonal_mean_bounds line 117
8. theorem OAI.SKGap.goe_path_spectral_tail line 130
9. def OAI.SKGap.pathBound line 190
10. def OAI.SKGap.pathLip line 192
11. lemma OAI.SKGap.path_constants_nonneg line 195
12. lemma OAI.SKGap.path_constants_bound line 203
13. lemma OAI.SKGap.matrixCoordinates_dimension_bound line 230
14. lemma OAI.SKGap.path_goodSet_failure line 240