OAI/Probability/SKGap/Localization/PositiveRamp.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Regression.positiveRamp line 66
2. def OAI.SKGapCutoff.Regression.positiveIndicator line 67
3. def OAI.SKGapCutoff.Regression.boundaryRamp line 68
4. lemma OAI.SKGapCutoff.Regression.positiveRamp_bounds line 71
5. lemma OAI.SKGapCutoff.Regression.positiveRamp_eq_zero line 75
6. lemma OAI.SKGapCutoff.Regression.positiveRamp_lipschitz line 79
7. lemma OAI.SKGapCutoff.Regression.positiveIndicator_measurable line 87
8. lemma OAI.SKGapCutoff.Regression.positiveIndicator_bounds line 91
9. lemma OAI.SKGapCutoff.Regression.boundaryRamp_bounds line 95
10. lemma OAI.SKGapCutoff.Regression.positiveRamp_error line 106
11. lemma OAI.SKGapCutoff.Regression.positiveRamp_tendsto line 115
12. lemma OAI.SKGapCutoff.Regression.boundaryRamp_tendsto line 127
13. lemma OAI.SKGapCutoff.Regression.boundaryRamp_lipschitz line 137
14. lemma OAI.SKGapCutoff.Regression.boundaryRamp_integral_tendsto line 161
15. lemma OAI.SKGapCutoff.Regression.positiveRamp_mul_integral_tendsto line 182
16. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.threshold_average line 200