vandermonde_transpose_mul_vandermonde

English

The transpose of Vandermonde(v) multiplied by Vandermonde(v) has entries equal to sums of powers: ((vandermonde v)^T (vandermonde v))_{i j} = sum_k v(k)^{i+j}.

Русский

Транспонированная Vandermonde(v) умноженная на Vandermonde(v) имеет элементы, равные суммам степеней: \$\\sum_k v(k)^{i+j}\$.

LaTeX

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

Lean4

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

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