OAI/Probability/SKGap/Terminal/PairRationalBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.list_prod_perturb line 12
2. lemma OAI.SKGap.list_prod_between line 36
3. lemma OAI.SKGap.pair_factor_control line 50
4. lemma OAI.SKGap.pair_square_factor_control line 60
5. def OAI.SKGap.pairRationalWeight line 71
6. lemma OAI.SKGap.pairRationalWeight_bounds line 74
7. def OAI.SKGap.pairK line 146
8. def OAI.SKGap.pairR line 148
9. def OAI.SKGap.pairCrossPolynomial line 151
10. lemma OAI.SKGap.abs_mul_le_one_pair line 155
11. lemma OAI.SKGap.pairK_bounds line 159
12. lemma OAI.SKGap.pairR_bounds line 205
13. lemma OAI.SKGap.pairKR_lower line 241