OAI/Probability/SKGap/Entropy/ProdFst.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Regression.ExponentiallyRare.prod_fst line 64
2. lemma OAI.SKGapCutoff.Regression.ExponentialSquareTails.prod_fst line 77
3. lemma OAI.SKGapCutoff.Regression.ExponentialConvergence.prod_fst line 87
4. lemma OAI.SKGapCutoff.Regression.exponentialSquareTails_of_bounded line 96
5. lemma OAI.SKGapCutoff.Regression.ExponentialSquareTails.scalar_mul line 111
6. lemma OAI.SKGapCutoff.Regression.ExponentialSquareTails.sum line 144
7. lemma OAI.SKGapCutoff.Regression.integrable_mul_of_sq line 159
8. lemma OAI.SKGapCutoff.Regression.integrable_add_sq line 169
9. lemma OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.lipschitz_secondMoment line 179
10. lemma OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.product_average line 198
11. lemma OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.unbounded_gram line 238