OAI/Combinatorics/Progressions/Polynomial/IntegerPolynomialActiveProfileSupport.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.monomialExponentSet line 15
  2. def OAI.Erdos3.scaledAffinePolynomial line 20
  3. theorem OAI.Erdos3.scaledAffinePolynomial_support line 24
  4. theorem OAI.Erdos3.scaledAffinePolynomial_coeff line 32
  5. theorem OAI.Erdos3.scaledAffinePolynomial_normalized_coeff line 38
  6. theorem OAI.Erdos3.fixedNonprincipalExponents_degree line 45
  7. theorem OAI.Erdos3.monomial_abs_le_scale line 65
  8. theorem OAI.Erdos3.monomialArrayPolynomial_box_bound line 75
  9. theorem OAI.Erdos3.monomialArrayPolynomial_box_budget line 86
  10. theorem OAI.Erdos3.scaledAffinePolynomial_box_bound line 92
  11. def OAI.Erdos3.integerMonomialArrayPolynomial line 116
  12. theorem OAI.Erdos3.integerMonomialArrayPolynomial_map line 120
  13. theorem OAI.Erdos3.integerMonomialArrayPolynomial_normalized_eval line 127
  14. theorem OAI.Erdos3.integerMonomialArrayPolynomial_degree line 139
  15. theorem OAI.Erdos3.modularMonomialArrayPolynomial_selected line 156
  16. def OAI.Erdos3.modularBoundedCoefficientPolynomial line 186
  17. theorem OAI.Erdos3.modularBoundedCoefficientPolynomial_degree line 191
  18. theorem OAI.Erdos3.modularBoundedCoefficientPolynomial_integer_reduce line 200
  19. def OAI.Erdos3.modularUnselectedCoefficientPolynomial line 207
  20. theorem OAI.Erdos3.modularBoundedCoefficientPolynomial_selected line 213
  21. theorem OAI.Erdos3.modularBoundedCoefficientPolynomial_selected_top line 241
  22. theorem OAI.Erdos3.exists_integerPolynomial_remainder line 266
  23. theorem OAI.Erdos3.integerPolynomial_remainder_eval line 282
  24. theorem OAI.Erdos3.integerMonomialArrayPolynomial_principal_sum line 301
  25. theorem OAI.Erdos3.productBlockExponent_monomial_int line 318
  26. theorem OAI.Erdos3.integerPrincipalPolynomial_eval line 325
  27. theorem OAI.Erdos3.small_coordinate_lift_unique line 357
  28. theorem OAI.Erdos3.integerPolynomial_remainder_identifies_lifts line 375
  29. def OAI.Erdos3.integerPolynomialCoordinatePMF line 416
  30. theorem OAI.Erdos3.integerPolynomialCoordinatePMF_bound line 426
  31. theorem OAI.Erdos3.integerPolynomialCoordinatePMF_box line 453
  32. def OAI.Erdos3.integerPolynomialLaw line 464
  33. theorem OAI.Erdos3.integerPolynomialLaw_probability line 467
  34. theorem OAI.Erdos3.integerPolynomialLaw_density line 473
  35. theorem OAI.Erdos3.integerPolynomialLaw_ae_box line 479
  36. theorem OAI.Erdos3.integerPolynomialCoordinatePMF_active_profile_bound line 513