OAI/NumberTheory/Ostmann/Arithmetic/MovingSlotPolynomials.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Actual slot products in the moving-giant line polynomials

Lists retain multiplicities: an ancestral compensation prime may occur in several descendant regular products. No squarefree polynomial is substituted.

  1. def OAI.Ostmann.movingSlotProduct line 14
  2. def OAI.Ostmann.movingSlotCoefficient line 17
  3. theorem OAI.Ostmann.movingSlotProduct_eval line 20
  4. theorem OAI.Ostmann.movingSlotCoefficient_eval line 27
  5. theorem OAI.Ostmann.movingSlotProduct_degree line 34
  6. theorem OAI.Ostmann.movingSlotCoefficient_degree line 44
  7. theorem OAI.Ostmann.movingSlotProduct_vars line 49
  8. theorem OAI.Ostmann.movingSlotCoefficient_vars line 62
  9. theorem OAI.Ostmann.movingSlotProduct_abs_le line 71
  10. theorem OAI.Ostmann.movingSlotCoefficient_abs_le line 84
  11. theorem OAI.Ostmann.movingSlotCoefficient_ne_zero line 93
  12. structure OAI.Ostmann.MovingSlotReversal line 106

    Source documentation

    The products multiplying the current two giants, together with the actual compensation product in the denominator. Giants themselves are excluded.

    structure MovingSlotReversal (σ : Type*) where
…
  13. def OAI.Ostmann.MovingSlotReversal.polynomial line 117
  14. def OAI.Ostmann.MovingSlotReversal.lengthLE line 123
  15. def OAI.Ostmann.MovingSlotReversal.frequencyLE line 126
  16. theorem OAI.Ostmann.MovingSlotReversal.polynomial_degree line 130
  17. theorem OAI.Ostmann.MovingSlotReversal.polynomial_height line 138
  18. theorem OAI.Ostmann.MovingSlotReversal.polynomial_units line 151