OAI/Combinatorics/Progressions/Polynomial/PolynomialCoefficientNormalization.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.roundedIntegerPolynomial line 17
  2. theorem OAI.Erdos3.roundedIntegerPolynomial_coeff line 20
  3. theorem OAI.Erdos3.roundedIntegerPolynomial_real_degree line 23
  4. theorem OAI.Erdos3.roundedIntegerPolynomial_remainder_bound line 36
  5. def OAI.Erdos3.slotPolynomialInput line 50
  6. theorem OAI.Erdos3.slotPolynomialInput_update line 53
  7. def OAI.Erdos3.slotAddShearEquiv line 66
  8. def OAI.Erdos3.polynomialSlotShear line 84
  9. theorem OAI.Erdos3.polynomialSlotShear_apply line 89
  10. theorem OAI.Erdos3.polynomialSlotShear_cast line 94
  11. theorem OAI.Erdos3.finsupp_weight_add_function line 124
  12. theorem OAI.Erdos3.weightedSupportLE_of_weight_le line 129
  13. theorem OAI.Erdos3.weightedTopPart_preserves_degree line 138
  14. theorem OAI.Erdos3.weightedTopPart_remainder_lt line 146
  15. def OAI.Erdos3.patchSlotWeight line 160
  16. def OAI.Erdos3.patchParameterWeight line 163
  17. theorem OAI.Erdos3.patchVariableWeight_split line 166
  18. def OAI.Erdos3.PolynomialSlots.topPart line 175
  19. theorem OAI.Erdos3.PolynomialSlots.topPart_homogeneous line 179
  20. theorem OAI.Erdos3.PolynomialSlots.sub_topPart_lower line 183
  21. theorem OAI.Erdos3.PolynomialSlots.topPart_parameter_exponent_zero line 190
  22. theorem OAI.Erdos3.PolynomialSlots.topPart_slots_independent line 205
  23. theorem OAI.Erdos3.PolynomialSlots.topPart_coeff_bound line 219
  24. def OAI.Erdos3.slotPrefixLift line 240
  25. theorem OAI.Erdos3.slotPrefixLift_degree line 244
  26. theorem OAI.Erdos3.slotPrefixLift_eval line 251
  27. theorem OAI.Erdos3.slotPrefixLift_self line 267
  28. def OAI.Erdos3.slotShearSubstitution line 279
  29. theorem OAI.Erdos3.slotShearSubstitution_degree line 285
  30. theorem OAI.Erdos3.slotShearSubstitution_before line 303
  31. theorem OAI.Erdos3.slotShearSubstitution_eval line 317
  32. def OAI.Erdos3.PolynomialSlots.shear line 349
  33. theorem OAI.Erdos3.PolynomialSlots.shear_center_before line 366
  34. theorem OAI.Erdos3.PolynomialSlots.shear_center_self line 376
  35. theorem OAI.Erdos3.PolynomialSlots.shear_center_eval line 385
  36. theorem OAI.Erdos3.PolynomialSlots.shear_integer_residual line 406
  37. def OAI.Erdos3.slotPolynomialLift line 439
  38. theorem OAI.Erdos3.slotPolynomialLift_degree line 442
  39. theorem OAI.Erdos3.slotPolynomialLift_lower line 453
  40. theorem OAI.Erdos3.slotPolynomialLift_eval line 464
  41. def OAI.Erdos3.PolynomialSlots.specializeCenter line 476
  42. theorem OAI.Erdos3.PolynomialSlots.specializeCenter_degree line 479
  43. theorem OAI.Erdos3.PolynomialSlots.specializeCenter_full_degree line 487
  44. theorem OAI.Erdos3.PolynomialSlots.topPart_aeval_independent line 495
  45. theorem OAI.Erdos3.PolynomialSlots.topPart_lift_specialize line 507
  46. theorem OAI.Erdos3.PolynomialSlots.exists_coefficient_normalized_prefix line 544
  47. theorem OAI.Erdos3.PolynomialSlots.exists_coefficient_normalized line 586
  48. theorem OAI.Erdos3.PolynomialPatch.exists_coefficient_normalized line 601