OAI/Probability/SKGap/Matrix/GOEResidualCov.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.goeRegressionResidual line 15
2. lemma OAI.SKGap.goe_cross_row_dot line 18
3. lemma OAI.SKGap.goeRegressionResidual_cov line 24
4. lemma OAI.SKGap.goeRegressionResidual_gaussian line 51
5. lemma OAI.SKGap.goeRegressionResidual_mean line 56
6. def OAI.SKGap.blockCoefficient line 73
7. lemma OAI.SKGap.blockCoefficient_sample line 77
8. lemma OAI.SKGap.goeBlockResidual_gaussian line 86
9. lemma OAI.SKGap.goeBlockResidual_mean line 93
10. lemma OAI.SKGap.block_regression_cov_algebra line 102
11. theorem OAI.SKGap.goe_regression_residual_law line 118