OAI/Combinatorics/Progressions/Estimates/CoefficientModeLowerTerms.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.fullShiftExponent_multinomial line 15
  2. theorem OAI.Erdos3.full_coefficient_sum_X_pow line 20
  3. theorem OAI.Erdos3.affineShiftPullback_diagonal_homogeneous line 26
  4. theorem OAI.Erdos3.polynomialTopSymbol_diagonal line 38
  5. theorem OAI.Erdos3.polynomialTopSymbol_add line 54
  6. theorem OAI.Erdos3.polynomialTopSymbol_eq_zero_of_degree_lt line 60
  7. theorem OAI.Erdos3.polynomialTopSymbol_add_lower line 66
  8. theorem OAI.Erdos3.full_coefficient_linear_pow line 82
  9. theorem OAI.Erdos3.linear_pow_totalDegree_le line 90
  10. theorem OAI.Erdos3.linear_power_full_difference line 102
  11. theorem OAI.Erdos3.linear_power_full_difference_algebra line 113
  12. theorem OAI.Erdos3.VectorPolynomial.homogeneous_substitute_scaled line 133
  13. theorem OAI.Erdos3.VectorPolynomial.homogeneous_substitute_scaled_functional line 150
  14. theorem OAI.Erdos3.VectorPolynomial.homogeneous_mode_diagonal_difference line 168
  15. theorem OAI.Erdos3.VectorPolynomial.homogeneous_mode_diagonal_contractedRow line 198
  16. theorem OAI.Erdos3.VectorPolynomial.coefficientModePolynomial_top_diagonal line 220
  17. theorem OAI.Erdos3.VectorPolynomial.coefficientModePolynomial_top_contractedRow line 248
  18. theorem OAI.Erdos3.VectorPolynomial.coefficientModePolynomial_top_integer_row line 256
  19. theorem OAI.Erdos3.VectorPolynomial.coefficient_mode_site_cauchySchwarz line 286
  20. theorem OAI.Erdos3.VectorPolynomial.coefficientModePolynomial_add_lower_top_diagonal line 316
  21. theorem OAI.Erdos3.VectorPolynomial.coefficient_mode_with_lower_site_cauchySchwarz line 327