OAI/Combinatorics/Progressions/Polynomial/PreparedComparisonGridPolynomialBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.preparedComparisonSourcePolynomial line 10
2. def OAI.Erdos3.VectorPolynomial.preparedComparisonGridPolynomial line 13
3. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonSourcePolynomial_nonneg line 18
4. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonGridPolynomial_nonneg line 23
5. theorem OAI.Erdos3.VectorPolynomial.slicedComparisonSourceLog_le_preparedComparisonSourcePolynomial line 40
6. theorem OAI.Erdos3.VectorPolynomial.comparisonGridLog_le_preparedComparisonGridPolynomial line 55