English
The evaluation of polyOfInterest against two Witt vectors x,y is expressed as a combination of the product (x*y) at level n+1, their level-n+1 components, and certain Witt-structured sums. It gives a concrete formula for peval at (x,y).
Русский
Оценка polyOfInterest по двум Witt-векторами x,y выражается через сочетание произведения (x*y) на уровне n+1, их компонентов на уровне n+1 и определенных Witt-структурированных сумм. Это конкретная формула для peval.
LaTeX
$$$\text{peval}(polyOfInterest\ p\ n)\!\big( ![x_0, x_1], ![y_0, y_1] \big) = (x*y)_{n+1} + p^{n+1} x_{n+1} y_{n+1} - y_{n+1} \sum_{i=0}^{n+1} p^{i} x_i^{p^{n+1-i}} - x_{n+1} \sum_{i=0}^{n+1} p^{i} y_i^{p^{n+1-i}}$$
Lean4
theorem peval_polyOfInterest (n : ℕ) (x y : 𝕎 k) :
peval (polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i] =
(x * y).coeff (n + 1) + p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), p ^ i * x.coeff i ^ p ^ (n + 1 - i) -
x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), p ^ i * y.coeff i ^ p ^ (n + 1 - i) :=
by
simp only [polyOfInterest, peval, Function.uncurry_apply_pair, aeval_X, Matrix.cons_val_one, map_mul,
Matrix.cons_val_zero, map_sub]
rw [sub_sub, add_comm (_ * _), ← sub_sub]
simp [wittPolynomial_eq_sum_C_mul_X_pow, aeval, mul_coeff, peval, map_natCast, map_add, map_pow, map_mul]
