OAI/Combinatorics/SumProduct/Alignment/CoefficientPeeling01.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoefficientPeeling.NearInteger line 21
2. lemma OAI.CoefficientPeeling.NearInteger.mul_nat line 23
3. lemma OAI.CoefficientPeeling.NearInteger.mono line 31
4. lemma OAI.CoefficientPeeling.tail_term_bound line 38
5. theorem OAI.CoefficientPeeling.peel line 60
6. theorem OAI.CoefficientPeeling.unit_or_rough line 92
7. lemma OAI.CoefficientPeeling.affine_coefficient line 105
8. structure OAI.PositiveCoefficientDescent.Input line 129
9. def OAI.PositiveCoefficientDescent.Controlled line 154
10. lemma OAI.PositiveCoefficientDescent.Controlled.mono line 161
11. lemma OAI.PositiveCoefficientDescent.step_cast line 167
12. lemma OAI.PositiveCoefficientDescent.sample_le line 176
13. theorem OAI.PositiveCoefficientDescent.eventual_rational_coefficients line 186