OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticSlotProducts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Frequency times products of the actual small slots

Slot lists retain multiplicities. These are the coefficient polynomials used in the ancestor reversals, so their degree and magnitude bounds come from the number and size of the original slots.

  1. def OAI.Ostmann.slotProduct line 14
  2. def OAI.Ostmann.frequencySlotProduct line 18
  3. theorem OAI.Ostmann.slotProduct_eval line 21
  4. theorem OAI.Ostmann.frequencySlotProduct_eval line 30
  5. theorem OAI.Ostmann.slotProduct_degree_le line 38
  6. theorem OAI.Ostmann.frequencySlotProduct_degree_le line 47
  7. theorem OAI.Ostmann.slotProduct_vars_subset line 53
  8. theorem OAI.Ostmann.frequencySlotProduct_vars_subset line 63
  9. theorem OAI.Ostmann.slotProduct_value_le line 70
  10. theorem OAI.Ostmann.frequencySlotProduct_value_le line 82
  11. theorem OAI.Ostmann.frequencySlotProduct_ne_zero line 90