English
Let v : Fin n → R and p : Fin n → R[X] with deg(p_i) ≤ i for all i. Then the matrix (p_j(v_i)) equals Vandermonde(v) times the matrix of coefficients (p_j)^{(i)}.
Русский
Пусть v: Fin n → R и p: Fin n → R[X] такие, что deg(p_i) ≤ i. Тогда матрица (p_j(v_i)) равна Vandermonde(v) умноженной на матрицу коэффициентов (p_j)^{(i)}.
LaTeX
$$$\\text{Matrix.of}(\\lambda i j, p_j(v_i)) = \\text{vandermonde}(v) \\cdot \\text{Matrix.of}(\\lambda i j, (p_j)^{\\text{coeff}_i}).$$$
Lean4
theorem eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials (v : Fin n → R) (p : Fin n → R[X])
(h_deg : ∀ i, (p i).natDegree ≤ i) :
Matrix.of (fun i j => ((p j).eval (v i))) =
(Matrix.vandermonde v) * (Matrix.of (fun (i j : Fin n) => (p j).coeff i)) :=
by
ext i j
simp_rw [Matrix.mul_apply, eval, Matrix.of_apply, eval₂]
simp only [Matrix.vandermonde]
have : (p j).support ⊆ range n := supp_subset_range <| Nat.lt_of_le_of_lt (h_deg j) <| Fin.prop j
rw [sum_eq_of_subset _ (fun j => zero_mul ((v i) ^ j)) this, ← Fin.sum_univ_eq_sum_range]
congr
ext k
rw [mul_comm, Matrix.of_apply, RingHom.id_apply]
