OAI/Probability/SKGap/Gaussian/GaussianRegression.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SKGap.GaussianRegression.law_eq_of_mean_covariance line 13
2. def OAI.SKGap.GaussianRegression.matrixCLM line 48
3. lemma OAI.SKGap.GaussianRegression.matrixCLM_apply line 51
4. theorem OAI.SKGap.GaussianRegression.residual_independent line 54
5. lemma OAI.SKGap.coordinate_hasLaw line 85
6. lemma OAI.SKGap.coordinates_gaussian line 90
7. lemma OAI.SKGap.coordinate_covariance line 95
8. lemma OAI.SKGap.linear_gaussian_mean line 107
9. lemma OAI.SKGap.linear_gaussian_covariance line 112
10. lemma OAI.SKGap.matrix_sample_gaussian line 121
11. lemma OAI.SKGap.matrix_sample_covariance line 125