OAI/Probability/SKGap/Matrix/DoublePlantedGOEArray.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Regression.doublePlantedGOEArray line 77
2. lemma OAI.SKGapCutoff.Regression.doublePlantedGOEArray_gaussian line 81
3. lemma OAI.SKGapCutoff.Regression.sampled_double_planted_gaussian line 85
4. lemma OAI.SKGapCutoff.Regression.doublePlantedGOEArray_mean line 93
5. lemma OAI.SKGapCutoff.Regression.sampled_double_planted_mean line 104
6. lemma OAI.SKGapCutoff.Regression.doublePlantedGOEArray_covariance line 115
7. lemma OAI.SKGapCutoff.Regression.sampled_double_planted_covariance line 127
8. lemma OAI.SKGapCutoff.Regression.double_planted_matrix_representation line 149