vandermonde_mul_vandermonde_transpose

English

The product Vandermonde(v) times the transpose of Vandermonde(w) yields entries given by a finite sum of powers: (vandermonde v) (vandermonde w)^T)_{i j} = sum_k (v(i) w(j))^k.

Русский

Произведение Vandermonde(v) на транспонированную Vandermonde(w) даёт элементы, равные сумме по k от степеней (v(i) w(j))^k.

LaTeX

$$$(\\mathrm{vandermonde} \\, v) \\cdot (\\mathrm{vandermonde} \\, w)^{T})_{i j} = \\sum_{k \\in \\mathrm{Fin}\, n} (v(i) \\cdot w(j))^{k}$$$

Lean4

theorem vandermonde_mul_vandermonde_transpose (v w : Fin n → R) (i j) :
    (vandermonde v * (vandermonde w)ᵀ) i j = ∑ k : Fin n, (v i * w j) ^ (k : ℕ) := by
  simp only [vandermonde_apply, Matrix.mul_apply, Matrix.transpose_apply, mul_pow]

Похожие утверждения