OAI/Probability/SKGap/Gaussian/SquareTail2.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Regression.gaussian_integrable_exp_quarter_sq line 62
2. lemma OAI.SKGapCutoff.Regression.iid_upper_deviation_of_log_mgf line 78
3. def OAI.SKGapCutoff.Regression.squareTail line 111
4. lemma OAI.SKGapCutoff.Regression.squareTail_nonneg line 113
5. lemma OAI.SKGapCutoff.Regression.squareTail_le line 117
6. lemma OAI.SKGapCutoff.Regression.measurable_squareTail line 121
7. lemma OAI.SKGapCutoff.Regression.integrable_exp_squareTail line 126
8. lemma OAI.SKGapCutoff.Regression.tendsto_squareTail_mgf line 134
9. def OAI.SKGapCutoff.Regression.ExponentialSquareTails line 154
10. theorem OAI.SKGapCutoff.Regression.iid_exponential_squareTails line 159
11. theorem OAI.SKGapCutoff.Regression.gaussian_exponential_squareTails line 200
12. lemma OAI.SKGapCutoff.Regression.squareTail_perturbation line 206
13. theorem OAI.SKGapCutoff.Regression.ExponentialSquareTails.l2_stability line 220
14. lemma OAI.SKGapCutoff.Regression.squareTail_add line 250
15. lemma OAI.SKGapCutoff.Regression.squareTail_antitone line 269
16. theorem OAI.SKGapCutoff.Regression.ExponentialSquareTails.add line 274
17. lemma OAI.SKGapCutoff.Regression.squareTail_mul line 308
18. lemma OAI.SKGapCutoff.Regression.ExponentialSquareTails.bounded_mul line 321
19. def OAI.SKGapCutoff.Regression.clippedSquare line 344
20. lemma OAI.SKGapCutoff.Regression.clippedSquare_bounds line 346
21. lemma OAI.SKGapCutoff.Regression.clippedSquare_error line 354
22. lemma OAI.SKGapCutoff.Regression.clippedSquare_lipschitz line 362
23. lemma OAI.SKGapCutoff.Regression.integrable_clippedSquare line 375
24. lemma OAI.SKGapCutoff.Regression.tendsto_integral_clippedSquare line 382
25. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.secondMoment line 399
26. lemma OAI.SKGapCutoff.Regression.iIndepFun_comp_hasLaw line 454
27. lemma OAI.SKGapCutoff.Regression.adaptive_innovation_error_exponential line 463