OAI/Combinatorics/Progressions/Polynomial/PolynomialGridValues.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_slow_polynomial_metric_budget line 12
2. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomial_coordinate_totalDegree line 81
3. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSlowBound_value line 94
4. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSlowBound_difference line 114
5. theorem OAI.Erdos3.exists_rational_polynomial_of_grid line 152
6. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialRationalGrid_exists_coordinates line 189
7. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSlowBound_dist_le line 241
8. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_polynomialSlowBound_dist_exp line 271
9. theorem OAI.Erdos3.polynomial_integer_value_common_denominator line 319
10. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialRationalGrid_value line 337