OAI/Probability/SKGap/Localization/ResidualRecipe.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Regression.linear_combination_lipschitz line 60
2. lemma OAI.SKGapCutoff.Regression.linear_combination_coefficient_bound line 78
3. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.linear_combination line 94
4. lemma OAI.SKGapCutoff.Regression.integral_quadratic_expansion line 108
5. lemma OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.linear_combination_energy line 132
6. def OAI.SKGapCutoff.Regression.residualRecipe line 151
7. lemma OAI.SKGapCutoff.Regression.ExponentialConvergence.residual_coefficients line 155
8. lemma OAI.SKGapCutoff.Regression.residualRecipe_eq_option line 167
9. lemma OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.residual line 173
10. lemma OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.residual_energy line 196
11. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.normalized_residual line 216
12. lemma OAI.SKGapCutoff.Regression.ExponentialConvergence.positive_rare line 250
13. lemma OAI.SKGapCutoff.Regression.empirical_normalized_square line 262
14. def OAI.SKGapCutoff.Regression.empiricalProjection line 274
15. def OAI.SKGapCutoff.Regression.limitingProjection line 279
16. lemma OAI.SKGapCutoff.Regression.empirical_residual_orthogonal line 284
17. lemma OAI.SKGapCutoff.Regression.ExponentialConvergence.nonzero_rare line 310
18. lemma OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.singular_gram_rare line 321
19. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.gram_residual line 335