OAI/Probability/SKRatio/Gaussian/EmpiricalIntervals.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioClock.Regression.cdfRamp line 12
2. lemma OAI.SKRatioClock.Regression.cdfRamp_bounds line 14
3. lemma OAI.SKRatioClock.Regression.cdfRamp_lipschitz line 18
4. lemma OAI.SKRatioClock.Regression.cdfRamp_sandwich line 35
5. lemma OAI.SKRatioClock.Regression.integrable_cdfRamp line 54
6. lemma OAI.SKRatioClock.Regression.integral_cdfRamp_bounds line 59
7. lemma OAI.SKRatioClock.Regression.continuous_measureReal_Iic line 67
8. theorem OAI.SKRatioClock.Regression.ExponentialEmpiricalConcentration.Iic line 75
9. lemma OAI.SKRatioClock.Regression.ExponentialConvergence.congr_eventually line 121
10. lemma OAI.SKRatioClock.Regression.exponentialConvergence_const line 131
11. lemma OAI.SKRatioClock.Regression.indicator_Ioc_sub line 140
12. lemma OAI.SKRatioClock.Regression.ExponentialEmpiricalConcentration.Ioc line 150
13. lemma OAI.SKRatioClock.Regression.ExponentialEmpiricalConcentration.Ioi line 171