OAI/NumberTheory/Ostmann/Supply/TernaryProductPolynomial.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The generating polynomial for a finite ternary population

The differential equation below yields an elementary repeat-removal bound. It uses only y^3 = y, the identity satisfied by the oriented quadratic characters, and does not invoke partition inversion as an additional input.

  1. def OAI.Ostmann.ternaryProduct line 20
  2. theorem OAI.Ostmann.ternaryProduct_coeff line 23
  3. theorem OAI.Ostmann.distinct_tuple_product_coeff line 41
  4. theorem OAI.Ostmann.ternaryProduct_differential line 47
  5. theorem OAI.Ostmann.ternaryProduct_coeff_recurrence line 72
  6. def OAI.Ostmann.ternaryDistinct line 96
  7. theorem OAI.Ostmann.ternaryDistinct_zero line 99
  8. theorem OAI.Ostmann.ternaryDistinct_one line 103
  9. theorem OAI.Ostmann.ternaryDistinct_recurrence line 109