OAI/Combinatorics/Progressions/Polynomial/VectorPolynomialReconstruction.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.VectorPolynomial line 15
  2. def OAI.Erdos3.VectorPolynomial.coefficients line 23
  3. def OAI.Erdos3.VectorPolynomial.monomial line 27
  4. theorem OAI.Erdos3.VectorPolynomial.coefficients_tmul line 30
  5. theorem OAI.Erdos3.VectorPolynomial.coefficients_monomial line 35
  6. theorem OAI.Erdos3.VectorPolynomial.coefficients_symm_single line 44
  7. theorem OAI.Erdos3.VectorPolynomial.sum_monomial_coefficients line 49
  8. def OAI.Erdos3.VectorPolynomial.map line 56
  9. theorem OAI.Erdos3.VectorPolynomial.map_monomial line 59
  10. theorem OAI.Erdos3.VectorPolynomial.coefficients_map line 62
  11. def OAI.Erdos3.VectorPolynomial.DegreeLE line 68
  12. theorem OAI.Erdos3.VectorPolynomial.degreeLE_iff line 71
  13. theorem OAI.Erdos3.VectorPolynomial.DegreeLE.map line 78
  14. theorem OAI.Erdos3.VectorPolynomial.degreeLE_map_iff line 83
  15. def OAI.Erdos3.VectorPolynomial.eval line 89
  16. theorem OAI.Erdos3.VectorPolynomial.eval_tmul line 93
  17. theorem OAI.Erdos3.VectorPolynomial.eval_monomial line 96
  18. theorem OAI.Erdos3.VectorPolynomial.eval_map line 100
  19. def OAI.Erdos3.monomialScale line 117
  20. theorem OAI.Erdos3.monomialScale_zero line 120
  21. theorem OAI.Erdos3.monomialScale_pos line 123
  22. theorem OAI.Erdos3.one_le_monomialScale line 128
  23. theorem OAI.Erdos3.le_monomialScale_of_ne_zero line 133
  24. theorem OAI.Erdos3.monomialScale_add line 154
  25. def OAI.Erdos3.VectorPolynomial.multiplyVariable line 171
  26. theorem OAI.Erdos3.VectorPolynomial.multiplyVariable_tmul line 175
  27. theorem OAI.Erdos3.VectorPolynomial.coefficients_multiplyVariable line 178
  28. def OAI.Erdos3.VectorPolynomial.eulerSum line 190
  29. theorem OAI.Erdos3.VectorPolynomial.eulerSum_monomial line 194
  30. theorem OAI.Erdos3.VectorPolynomial.eulerSum_eq_degree_smul line 206
  31. def OAI.Erdos3.VectorPolynomial.reconstructDerivatives line 220
  32. theorem OAI.Erdos3.VectorPolynomial.reconstructDerivatives_apply line 224
  33. theorem OAI.Erdos3.VectorPolynomial.reconstructDerivatives_partial line 230
  34. theorem OAI.Erdos3.VectorPolynomial.coefficients_reconstructDerivatives line 240
  35. theorem OAI.Erdos3.VectorPolynomial.reconstructDerivatives_mem line 248
  36. theorem OAI.Erdos3.VectorPolynomial.reconstructDerivatives_homogeneous line 262
  37. theorem OAI.Erdos3.VectorPolynomial.homogeneous_derivative_split_mod line 281
  38. def OAI.Erdos3.VectorPolynomial.coefficientTensorBasis line 308
  39. theorem OAI.Erdos3.VectorPolynomial.coefficientTensorBasis_apply line 312
  40. theorem OAI.Erdos3.VectorPolynomial.coefficientTensorBasis_repr line 316
  41. def OAI.Erdos3.VectorPolynomial.coordinate line 338
  42. theorem OAI.Erdos3.VectorPolynomial.coeff_coordinate line 341
  43. theorem OAI.Erdos3.VectorPolynomial.coordinate_monomial line 348
  44. theorem OAI.Erdos3.VectorPolynomial.coordinate_sum line 357
  45. theorem OAI.Erdos3.VectorPolynomial.scalar_weightedDegree_le_iff line 363
  46. theorem OAI.Erdos3.VectorPolynomial.degreeLE_iff_coordinates line 372
  47. theorem OAI.Erdos3.VectorPolynomial.degreeLE_iff_basis_coordinates line 383
  48. theorem OAI.Erdos3.VectorPolynomial.degreeLE_one_iff_basis_totalDegree line 394
  49. def OAI.Erdos3.VectorPolynomial.pair line 414
  50. theorem OAI.Erdos3.VectorPolynomial.coefficients_pair line 418
  51. theorem OAI.Erdos3.VectorPolynomial.eval_pair line 422
  52. def OAI.Erdos3.VectorPolynomial.restrictCoefficients line 426
  53. theorem OAI.Erdos3.VectorPolynomial.coefficients_restrictCoefficients line 433
  54. theorem OAI.Erdos3.VectorPolynomial.map_restrictCoefficients line 439
  55. theorem OAI.Erdos3.VectorPolynomial.eval_restrictCoefficients line 446
  56. def OAI.Erdos3.VectorPolynomial.coefficientSupport line 462
  57. theorem OAI.Erdos3.VectorPolynomial.mem_coefficientSupport line 472
  58. theorem OAI.Erdos3.VectorPolynomial.coefficientSupport_mono line 475
  59. theorem OAI.Erdos3.VectorPolynomial.monomial_mem_coefficientSupport line 480
  60. theorem OAI.Erdos3.VectorPolynomial.coefficientSupport_inf line 487
  61. theorem OAI.Erdos3.VectorPolynomial.coefficientSupport_empty line 500
  62. def OAI.Erdos3.VectorPolynomial.ofScalar line 519
  63. theorem OAI.Erdos3.VectorPolynomial.coefficients_ofScalar line 522
  64. def OAI.Erdos3.VectorPolynomial.ofCoordinates line 529
  65. theorem OAI.Erdos3.VectorPolynomial.coefficients_ofCoordinates line 533
  66. theorem OAI.Erdos3.VectorPolynomial.coordinate_ofCoordinates line 538
  67. theorem OAI.Erdos3.VectorPolynomial.ofCoordinates_coordinate line 547
  68. def OAI.Erdos3.VectorPolynomial.coordinatesEquiv line 557