mathlib3 documentation

linear_algebra.vandermonde

Vandermonde matrix #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the vandermonde matrix and gives its determinant.

Main definitions #

Main results #

source
def matrix.vandermonde {R : Type u_1} [comm_ring R] {n : ℕ} (v : fin n → R) :
matrix (fin n) (fin n) R

vandermonde v is the square matrix with ith row equal to 1, v i, v i ^ 2, v i ^ 3, ....

Equations
source
@[simp]
theorem matrix.vandermonde_apply {R : Type u_1} [comm_ring R] {n : ℕ} (v : fin n → R) (i j : fin n) :
matrix.vandermonde v i j = v i ^ ↑j
source
@[simp]
theorem matrix.vandermonde_cons {R : Type u_1} [comm_ring R] {n : ℕ} (v0 : R) (v : fin n → R) :
matrix.vandermonde (fin.cons v0 v) = fin.cons (λ (j : fin (n + 1)), v0 ^ ↑j) (λ (i : fin n), fin.cons 1 (λ (j : fin n), v i * matrix.vandermonde v i j))
source
theorem matrix.vandermonde_succ {R : Type u_1} [comm_ring R] {n : ℕ} (v : fin n.succ → R) :
matrix.vandermonde v = fin.cons (λ (j : fin n.succ), v 0 ^ ↑j) (λ (i : fin n), fin.cons 1 (λ (j : fin n), v i.succ * matrix.vandermonde (fin.tail v) i j))
source
theorem matrix.vandermonde_mul_vandermonde_transpose {R : Type u_1} [comm_ring R] {n : ℕ} (v w : fin n → R) (i j : fin n) :
(matrix.vandermonde v).mul (matrix.vandermonde w).transpose i j = finset.univ.sum (λ (k : fin n), (v i * w j) ^ ↑k)
source
theorem matrix.vandermonde_transpose_mul_vandermonde {R : Type u_1} [comm_ring R] {n : ℕ} (v : fin n → R) (i j : fin n) :
(matrix.vandermonde v).transpose.mul (matrix.vandermonde v) i j = finset.univ.sum (λ (k : fin n), v k ^ (↑i + ↑j))
source
theorem matrix.det_vandermonde {R : Type u_1} [comm_ring R] {n : ℕ} (v : fin n → R) :
(matrix.vandermonde v).det = finset.univ.prod (λ (i : fin n), (finset.Ioi i).prod (λ (j : fin n), v j - v i))
source
theorem matrix.det_vandermonde_eq_zero_iff {R : Type u_1} [comm_ring R] [is_domain R] {n : ℕ} {v : fin n → R} :
(matrix.vandermonde v).det = 0 ↔ ∃ (i j : fin n), v i = v j ∧ i ≠ j
source
theorem matrix.det_vandermonde_ne_zero_iff {R : Type u_1} [comm_ring R] [is_domain R] {n : ℕ} {v : fin n → R} :
(matrix.vandermonde v).det ≠ 0 ↔ function.injective v
source
theorem matrix.eq_zero_of_forall_index_sum_pow_mul_eq_zero {R : Type u_1} [comm_ring R] [is_domain R] {n : ℕ} {f v : fin n → R} (hf : function.injective f) (hfv : ∀ (j : fin n), finset.univ.sum (λ (i : fin n), f j ^ ↑i * v i) = 0) :
v = 0
source
theorem matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero {R : Type u_1} [comm_ring R] [is_domain R] {n : ℕ} {f v : fin n → R} (hf : function.injective f) (hfv : ∀ (j : fin n), finset.univ.sum (λ (i : fin n), v i * f j ^ ↑i) = 0) :
v = 0
source
theorem matrix.eq_zero_of_forall_pow_sum_mul_pow_eq_zero {R : Type u_1} [comm_ring R] [is_domain R] {n : ℕ} {f v : fin n → R} (hf : function.injective f) (hfv : ∀ (i : fin n), finset.univ.sum (λ (j : fin n), v j * f j ^ ↑i) = 0) :
v = 0