English
There is a remainder term arising in the construction of Witt polynomial products; this remainder accounts for the difference between a truncated and full product.
Русский
Существует остаток в конструировании Witt-полиномов; остаток учитывает разницу между усечённым и полным произведением.
LaTeX
$$$\\text{remainder}(p,n) := \\sum_{i=0}^{n} p^i wittMul(p,i)^p^{(n-i)}$ (schematic definition in context).$$$
Lean4
/-- `remainder p n` represents the remainder term from `mul_polyOfInterest_aux3`.
`wittPolyProd p (n+1)` will have variables up to `n+1`,
but `remainder` will only have variables up to `n`.
-/
def remainder (n : ℕ) : 𝕄 :=
(∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) ((p : ℤ) ^ x))) *
∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) ((p : ℤ) ^ x))
