OAI/Combinatorics/Progressions/Polynomial/PolynomialIntegerInputs.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalPolynomialHeightLE line 19
  2. theorem OAI.Erdos3.RationalPolynomialHeightLE.mono line 26
  3. theorem OAI.Erdos3.RationalPolynomialHeightLE.one_le line 29
  4. theorem OAI.Erdos3.RationalPolynomialHeightLE.zero line 32
  5. theorem OAI.Erdos3.RationalPolynomialHeightLE.C line 36
  6. theorem OAI.Erdos3.RationalPolynomialHeightLE.X line 46
  7. theorem OAI.Erdos3.RationalPolynomialHeightLE.C_mul line 54
  8. theorem OAI.Erdos3.RationalPolynomialHeightLE.mul_X line 61
  9. theorem OAI.Erdos3.RationalPolynomialHeightLE.sum line 70
  10. theorem OAI.Erdos3.RationalPolynomialHeightLE.sum_finset line 78
  11. def OAI.Erdos3.polynomialDenominator line 99
  12. theorem OAI.Erdos3.polynomialDenominator_pos line 102
  13. theorem OAI.Erdos3.polynomialDenominator_le line 105
  14. def OAI.Erdos3.integralNumeratorPolynomial line 110
  15. theorem OAI.Erdos3.product_scaled_powers line 116
  16. theorem OAI.Erdos3.integralNumeratorPolynomial_eval line 122
  17. theorem OAI.Erdos3.abs_aeval_le_box_bound line 163
  18. theorem OAI.Erdos3.abs_aeval_sub_aeval_box_bound line 203
  19. theorem OAI.Erdos3.lipschitzOn_mvPolynomial_aeval_box line 238
  20. theorem OAI.Erdos3.monomialScale_mul_normalized_prod line 263
  21. theorem OAI.Erdos3.abs_eval_le_scaled_box_bound line 272
  22. theorem OAI.Erdos3.abs_eval_sub_eval_scaled_box_bound line 307
  23. theorem OAI.Erdos3.rational_polynomial_eval_sub_integer_multiple line 370
  24. def OAI.Erdos3.polynomialFamilyDenominator line 423
  25. theorem OAI.Erdos3.polynomialFamilyDenominator_pos line 426
  26. theorem OAI.Erdos3.polynomialDenominator_dvd_family line 430
  27. theorem OAI.Erdos3.polynomialDenominator_exp_bound line 434
  28. theorem OAI.Erdos3.polynomialFamilyDenominator_exp_bound line 449
  29. theorem OAI.Erdos3.rational_polynomial_family_eval_sub_mem_grid line 465
  30. theorem OAI.Erdos3.slowPolynomial_oscillation_on_slice line 489
  31. theorem OAI.Erdos3.exists_slowPolynomial_residueSlice line 519
  32. theorem OAI.Erdos3.polynomialFamilyDenominator_degree_budget line 548
  33. theorem OAI.Erdos3.polynomial_integer_value_denominator line 586
  34. theorem OAI.Erdos3.polynomial_family_integer_values_grid line 594
  35. theorem OAI.Erdos3.integer_difference_mem_grid line 610
  36. theorem OAI.Erdos3.polynomial_family_integer_congruence line 621