OAI/Probability/SKRatio/Gaussian/ExponentialEvents.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioClock.Regression.ExponentialEmpiricalConcentration line 11
2. def OAI.SKRatioClock.Regression.ExponentiallyRare line 20
3. lemma OAI.SKRatioClock.Regression.ExponentiallyRare.mono line 25
4. lemma OAI.SKRatioClock.Regression.ExponentiallyRare.union line 34
5. lemma OAI.SKRatioClock.Regression.exponentiallyRare_empty line 55
6. lemma OAI.SKRatioClock.Regression.ExponentiallyRare.iUnion_finite line 61
7. def OAI.SKRatioClock.Regression.ExponentialConvergence line 81
8. lemma OAI.SKRatioClock.Regression.ExponentialConvergence.continuous_map line 86
9. lemma OAI.SKRatioClock.Regression.ExponentialConvergence.prod line 101
10. lemma OAI.SKRatioClock.Regression.ExponentialConvergence.pi_finite line 112
11. lemma OAI.SKRatioClock.Regression.ExponentialEmpiricalConcentration.average line 130
12. lemma OAI.SKRatioClock.Regression.ExponentialEmpiricalConcentration.map line 141
13. lemma OAI.SKRatioClock.Regression.ExponentiallyRare.without_prefactor line 155