OAI/Probability/SKGap/Localization/QueryColumn.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Regression.clm_pi_expansion line 27
2. lemma OAI.SKGapCutoff.Regression.gaussian_mean_linear line 40
3. lemma OAI.SKGapCutoff.Regression.gaussian_variance_linear line 51
4. lemma OAI.SKGapCutoff.Regression.gaussian_vector_law_ext line 72
5. lemma OAI.SKGapCutoff.Regression.coordinate_mean line 88
6. lemma OAI.SKGapCutoff.Regression.goe_entry_mean line 92
7. lemma OAI.SKGapCutoff.Regression.sandwich_entry_mean line 99
8. def OAI.SKGapCutoff.Regression.queryColumn line 119
9. def OAI.SKGapCutoff.Regression.queryComplement line 121
10. lemma OAI.SKGapCutoff.Regression.queryColumn_unit line 124
11. lemma OAI.SKGapCutoff.Regression.queryComplement_symmetric line 132
12. lemma OAI.SKGapCutoff.Regression.queryComplement_mul_column line 136
13. lemma OAI.SKGapCutoff.Regression.queryComplement_sq line 141
14. def OAI.SKGapCutoff.Regression.queryInnovation line 153
15. def OAI.SKGapCutoff.Regression.queryInnovationCoefficient line 158
16. lemma OAI.SKGapCutoff.Regression.queryInnovation_as_linearTest line 163
17. lemma OAI.SKGapCutoff.Regression.queryInnovation_gaussian line 169
18. lemma OAI.SKGapCutoff.Regression.queryInnovation_mean line 179
19. lemma OAI.SKGapCutoff.Regression.queryInnovation_covariance line 186
20. def OAI.SKGapCutoff.Regression.queryAnswerCLM line 226
21. lemma OAI.SKGapCutoff.Regression.queryAnswerCLM_apply line 231
22. lemma OAI.SKGapCutoff.Regression.queryAnswer_covariance line 236
23. lemma OAI.SKGapCutoff.Regression.query_innovation_law line 246
24. def OAI.SKGapCutoff.Regression.freshRegressionCLM line 262
25. lemma OAI.SKGapCutoff.Regression.freshRegressionCLM_apply line 269
26. lemma OAI.SKGapCutoff.Regression.fresh_residual_independent line 276