OAI/Probability/SKGap/Entropy/ExponentiallyRare.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Regression.ExponentiallyRare line 56
2. lemma OAI.SKGapCutoff.Regression.ExponentiallyRare.mono line 61
3. lemma OAI.SKGapCutoff.Regression.ExponentiallyRare.union line 70
4. lemma OAI.SKGapCutoff.Regression.exponentiallyRare_empty line 91
5. lemma OAI.SKGapCutoff.Regression.ExponentiallyRare.iUnion_finite line 97
6. def OAI.SKGapCutoff.Regression.ExponentialConvergence line 117
7. lemma OAI.SKGapCutoff.Regression.ExponentialConvergence.continuous_map line 122
8. lemma OAI.SKGapCutoff.Regression.ExponentialConvergence.prod line 137
9. lemma OAI.SKGapCutoff.Regression.ExponentialConvergence.pi_finite line 148
10. lemma OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.average line 166
11. lemma OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.map line 177
12. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.parameter_map line 191
13. lemma OAI.SKGapCutoff.Regression.bounded_product_lipschitz line 250
14. lemma OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.gram line 271
15. lemma OAI.SKGapCutoff.Regression.ExponentialConvergence.matrix_inv line 291
16. lemma OAI.SKGapCutoff.Regression.ExponentialConvergence.matrix_mulVec line 302
17. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.projection_coefficients line 312