OAI/Computability/DeterministicSum/SparsePolynomials.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Monic remainders, sparse coefficient support and weighted polynomial identities.

  1. def OAI.DeterministicThreeSum.Sparse.gridPolynomial line 13
  2. lemma OAI.DeterministicThreeSum.Sparse.gridPolynomial_monic line 16
  3. lemma OAI.DeterministicThreeSum.Sparse.gridPolynomial_eval line 21
  4. lemma OAI.DeterministicThreeSum.Sparse.gridPolynomial_natDegree line 27
  5. def OAI.DeterministicThreeSum.Sparse.remainderPower line 34
  6. lemma OAI.DeterministicThreeSum.Sparse.remainderPower_eval line 37
  7. lemma OAI.DeterministicThreeSum.Sparse.remainderPower_degree_le line 44
  8. lemma OAI.DeterministicThreeSum.Sparse.remainderPower_degree_lt line 50
  9. lemma OAI.DeterministicThreeSum.Sparse.remainderPower_coeff_zero_of_ge line 60
  10. lemma OAI.DeterministicThreeSum.Sparse.remainderPower_coeff_zero_of_gt line 64
  11. lemma OAI.DeterministicThreeSum.Sparse.remainderPower_sum line 68
  12. def OAI.DeterministicThreeSum.Sparse.localCoefficient line 76
  13. lemma OAI.DeterministicThreeSum.Sparse.localCoefficient_zero line 80
  14. lemma OAI.DeterministicThreeSum.Sparse.localCoefficient_eval line 92
  15. def OAI.DeterministicThreeSum.Sparse.coefficient line 122
  16. lemma OAI.DeterministicThreeSum.Sparse.monomial_expansion line 126
  17. theorem OAI.DeterministicThreeSum.Sparse.coefficient_evaluation line 138
  18. lemma OAI.DeterministicThreeSum.Sparse.coefficient_support line 158
  19. lemma OAI.DeterministicThreeSum.Weighted.split_support line 185
  20. lemma OAI.DeterministicThreeSum.Weighted.weighted_finite_interchange line 218
  21. lemma OAI.DeterministicThreeSum.Weighted.weighted_split line 230
  22. def OAI.DeterministicThreeSum.Weighted.degree line 244
  23. def OAI.DeterministicThreeSum.Weighted.lowSet line 245
  24. def OAI.DeterministicThreeSum.Weighted.smallSet line 247
  25. def OAI.DeterministicThreeSum.Weighted.cutoff line 249
  26. def OAI.DeterministicThreeSum.Weighted.monomial line 251
  27. lemma OAI.DeterministicThreeSum.Weighted.source_support line 254
  28. def OAI.DeterministicThreeSum.Weighted.U line 269
  29. def OAI.DeterministicThreeSum.Weighted.W line 272
  30. theorem OAI.DeterministicThreeSum.Weighted.polynomial_group_identity line 276