OAI/Combinatorics/Progressions/Polynomial/MixedWeightedPolynomialRename.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.polynomialTranslate line 18
  2. theorem OAI.Erdos3.polynomialTranslate_X line 21
  3. theorem OAI.Erdos3.polynomialTranslate_C line 24
  4. def OAI.Erdos3.weightedSupportLE line 27
  5. def OAI.Erdos3.weightedSupportLT line 30
  6. theorem OAI.Erdos3.weightedSupportLE_monomial line 33
  7. theorem OAI.Erdos3.weightedSupportLE_mul line 40
  8. theorem OAI.Erdos3.weightedSupportLT_mul_LE line 48
  9. theorem OAI.Erdos3.weightedSupportLE_mul_LT line 56
  10. theorem OAI.Erdos3.translation_bounds_mul line 62
  11. theorem OAI.Erdos3.polynomialTranslate_monomial_bounds line 77
  12. def OAI.Erdos3.polynomialDegreeGap line 136
  13. theorem OAI.Erdos3.polynomialDegreeGap_monomial line 139
  14. theorem OAI.Erdos3.polynomialDegreeGap_mul line 143
  15. theorem OAI.Erdos3.polynomialDegreeGap_pderiv line 157
  16. def OAI.Erdos3.scalarDirectionalDerivative line 174
  17. theorem OAI.Erdos3.scalarDirectionalDerivative_apply line 178
  18. theorem OAI.Erdos3.scalarDirectionalDerivative_C line 184
  19. theorem OAI.Erdos3.scalarDirectionalDerivative_X line 187
  20. theorem OAI.Erdos3.scalarDirectionalDerivative_mul line 192
  21. theorem OAI.Erdos3.polynomialDegreeGap_directionalDerivative line 199
  22. theorem OAI.Erdos3.polynomialDegreeGap_translate_monomial line 205
  23. theorem OAI.Erdos3.polynomialDegreeGap_translate_sub_monomial line 211
  24. theorem OAI.Erdos3.eval₂_eq_of_weightedSupport line 229
  25. theorem OAI.Erdos3.aeval_eq_of_weightedSupportLE line 239
  26. theorem OAI.Erdos3.weightedSupportLE_mono line 258
  27. theorem OAI.Erdos3.weightedSupportLE_C line 262
  28. theorem OAI.Erdos3.weightedSupportLE_X line 266
  29. theorem OAI.Erdos3.weightedSupportLE_pow line 271
  30. theorem OAI.Erdos3.weightedSupportLE_prod line 279
  31. theorem OAI.Erdos3.weightedSupportLE_aeval_monomial line 291
  32. theorem OAI.Erdos3.weightedSupportLE_aeval line 305
  33. theorem OAI.Erdos3.mem_weightedSupportLE_iff line 315
  34. theorem OAI.Erdos3.weightedTotalDegree_aeval_le line 321
  35. def OAI.Erdos3.scalarTaylorRemainder line 343
  36. theorem OAI.Erdos3.scalarTaylorRemainder_apply line 347
  37. theorem OAI.Erdos3.scalarTaylorRemainder_C line 350
  38. theorem OAI.Erdos3.scalarTaylorRemainder_X line 354
  39. theorem OAI.Erdos3.scalarTaylorRemainder_mul line 359
  40. theorem OAI.Erdos3.remainder_monomial_add line 367
  41. theorem OAI.Erdos3.scalarTaylorRemainder_monomial line 385
  42. def OAI.Erdos3.polynomialTranslationPath line 417
  43. theorem OAI.Erdos3.polynomialTranslationPath_C line 422
  44. theorem OAI.Erdos3.polynomialTranslationPath_X line 426
  45. theorem OAI.Erdos3.polynomialTranslationPath_eval line 431
  46. theorem OAI.Erdos3.polynomialTranslate_zero line 445
  47. theorem OAI.Erdos3.polynomialTranslationPath_eval_zero line 452
  48. theorem OAI.Erdos3.polynomialTranslationPath_derivative line 459
  49. def OAI.Erdos3.lowestSlotWeight line 488
  50. theorem OAI.Erdos3.exponent_eq_single_of_lowest_slot line 490
  51. def OAI.Erdos3.SlotAffine line 510
  52. theorem OAI.Erdos3.SlotAffine.zero line 520
  53. theorem OAI.Erdos3.SlotAffine.add line 525
  54. theorem OAI.Erdos3.SlotAffine.of_monomial line 534
  55. theorem OAI.Erdos3.slotAffine_of_weightedSupport line 568
  56. theorem OAI.Erdos3.weightedSupportLE_rename_inl_ring line 595
  57. theorem OAI.Erdos3.weightedSupportLE_rename_inr_ring line 603