OAI/Combinatorics/Progressions/Estimates/BoundedCoefficientExpansion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.degreeLE_monomial_of_degree_le line 9
2. theorem OAI.Erdos3.VectorPolynomial.affineModeLift_zero_iff_bounded line 21
3. theorem OAI.Erdos3.VectorPolynomial.coefficientArrayFunctional_eq_zero_iff_trivial line 29
4. theorem OAI.Erdos3.VectorPolynomial.sum_bounded_monomial_coefficients line 62
5. theorem OAI.Erdos3.VectorPolynomial.coefficientFunctional_bounded_expansion line 84