OAI/Probability/SKGap/Gaussian/GaussianRankCorrection.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Regression.gaussianRankCorrection line 51
2. lemma OAI.SKGapCutoff.Regression.rankCorrection_sq_bound line 55
3. lemma OAI.SKGapCutoff.Regression.gaussian_linear_unit_tail line 69
4. theorem OAI.SKGapCutoff.Regression.gaussian_rank_correction_tail line 79
5. def OAI.SKGapCutoff.Regression.innovationErrorVectors line 126
6. def OAI.SKGapCutoff.Regression.innovationErrorCoefficients line 130
7. lemma OAI.SKGapCutoff.Regression.innovationErrorVectors_sq_le line 137
8. lemma OAI.SKGapCutoff.Regression.innovationErrorCoefficients_sq_le line 148
9. lemma OAI.SKGapCutoff.Regression.queryInnovation_error_eq line 157
10. theorem OAI.SKGapCutoff.Regression.queryInnovation_iid_error_tail line 178
11. lemma OAI.SKGapCutoff.Regression.probability_prod_section_bound line 192
12. theorem OAI.SKGapCutoff.Regression.adaptive_queryInnovation_iid_error_tail line 201
13. lemma OAI.SKGapCutoff.Regression.independent_bounded_average_tail line 234
14. lemma OAI.SKGapCutoff.Regression.average_Lipschitz_error_sq line 275
15. theorem OAI.SKGapCutoff.Regression.queryInnovation_empirical_tail line 298
16. lemma OAI.SKGapCutoff.Regression.measurable_residualProjection_comp line 371
17. theorem OAI.SKGapCutoff.Regression.adaptive_queryInnovation_empirical_tail line 385