English
The value succNthVal(p,n,a1,a2,bs,ha1,ha2) satisfies the defining relation given by succNthDefiningPoly; i.e., it is a root that yields the next coefficient in the recursion.
Русский
Значение succNthVal(p,n,a1,a2,bs,ha1,ha2) удовлетворяет задающемуRelation succNthDefiningPoly; то есть оно является корнем, задающим следующий коэффициент в рекурсии.
LaTeX
$$(succNthVal(p,n,a1,a2,bs,ha1,ha2))^p * a1.coeff 0^{p^{n+1}} + a1.coeff(n+1) (bs 0^p)^{p^{n+1}} + nthRemainder p n (fun v => bs v^p) (truncateFun (n+1) a1) = (succNthVal(p,n,a1,a2,bs,ha1,ha2)) * a2.coeff 0^{p^{n+1}} + a2.coeff(n+1) bs 0^{p^{n+1}} + nthRemainder p n bs (truncateFun (n+1) a2)$$
Lean4
theorem succNthVal_spec' (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) =
succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
nthRemainder p n bs (truncateFun (n + 1) a₂) :=
by
rw [← sub_eq_zero]
have := succNthVal_spec p n a₁ a₂ bs ha₁ ha₂
simp only [Polynomial.eval_X, Polynomial.eval_C, Polynomial.eval_pow, succNthDefiningPoly, Polynomial.eval_mul,
Polynomial.eval_add, Polynomial.eval_sub, Polynomial.IsRoot.def] at this
convert this using 1
ring
