OAI/Probability/SKGap/Localization/SampledFlatCLM.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Regression.gaussian_add_constant line 43
2. lemma OAI.SKGapCutoff.Regression.piGaussian_coordinates line 53
3. lemma OAI.SKGapCutoff.Regression.piGaussian_coordinate_mean line 58
4. lemma OAI.SKGapCutoff.Regression.piGaussian_coordinate_covariance line 63
5. lemma OAI.SKGapCutoff.Regression.upperCoefficient_min_max line 78
6. lemma OAI.SKGapCutoff.Regression.minmax_pair_eq_iff line 84
7. def OAI.SKGapCutoff.Regression.sampledFlatCLM line 89
8. lemma OAI.SKGapCutoff.Regression.sampledFlatCLM_apply line 93
9. def OAI.SKGapCutoff.Regression.plantedGOEArray line 98
10. def OAI.SKGapCutoff.Regression.offDiagonalGOECLM line 102
11. lemma OAI.SKGapCutoff.Regression.plantedGOEArray_gaussian line 106
12. lemma OAI.SKGapCutoff.Regression.sampled_planted_gaussian line 122
13. lemma OAI.SKGapCutoff.Regression.plantedGOEArray_mean line 130
14. lemma OAI.SKGapCutoff.Regression.sampled_planted_mean line 140
15. lemma OAI.SKGapCutoff.Regression.plantedGOEArray_covariance line 150
16. lemma OAI.SKGapCutoff.Regression.sampled_planted_covariance line 167
17. lemma OAI.SKGapCutoff.Regression.planted_matrix_representation line 190