Vandermonde matrix

This file defines the vandermonde matrix and gives its determinant.

Main definitions

• vandermonde v: a square matrix with the i, jth entry equal to v i ^ j.

Main results

• det_vandermonde: det (vandermonde v) is the product of v i - v j, where (i, j) ranges over the unordered pairs.

def Matrix.vandermonde {R : Type u_1} [CommRing 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

• Matrix.vandermonde v i j = v i ^ ↑j

@[simp]

theorem Matrix.vandermonde_apply {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) (i : Fin n) (j : Fin n) : Matrix.vandermonde v i j = v i ^ ↑j

@[simp]

theorem Matrix.vandermonde_cons {R : Type u_1} [CommRing R] {n : ℕ} (v0 : R) (v : Fin n → R) : Matrix.vandermonde (Fin.cons v0 v) = Fin.cons (fun (j : Fin (Nat.succ n)) => v0 ^ ↑j) fun (i : Fin n) => Fin.cons 1 fun (j : Fin n) => v i * Matrix.vandermonde v i j

theorem Matrix.vandermonde_succ {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin (Nat.succ n) → R) : Matrix.vandermonde v = Fin.cons (fun (j : Fin (Nat.succ n)) => v 0 ^ ↑j) fun (i : Fin n) => Fin.cons 1 fun (j : Fin n) => v (Fin.succ i) * Matrix.vandermonde (Fin.tail v) i j

theorem Matrix.vandermonde_mul_vandermonde_transpose {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) (w : Fin n → R) (i : Fin n) (j : Fin n) : (Matrix.vandermonde v * Matrix.transpose (Matrix.vandermonde w)) i j = Finset.sum Finset.univ fun (k : Fin n) => (v i * w j) ^ ↑k

theorem Matrix.vandermonde_transpose_mul_vandermonde {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) (i : Fin n) (j : Fin n) : (Matrix.transpose (Matrix.vandermonde v) * Matrix.vandermonde v) i j = Finset.sum Finset.univ fun (k : Fin n) => v k ^ (↑i + ↑j)

theorem Matrix.det_vandermonde {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) : Matrix.det (Matrix.vandermonde v) = Finset.prod Finset.univ fun (i : Fin n) => Finset.prod (Finset.Ioi i) fun (j : Fin n) => v j - v i

theorem Matrix.det_vandermonde_eq_zero_iff {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} {v : Fin n → R} : Matrix.det (Matrix.vandermonde v) = 0 ↔ ∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j

theorem Matrix.det_vandermonde_ne_zero_iff {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} {v : Fin n → R} : Matrix.det (Matrix.vandermonde v) ≠ 0 ↔ Function.Injective v

@[simp]

theorem Matrix.det_vandermonde_add {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) (a : R) : Matrix.det (Matrix.vandermonde fun (i : Fin n) => v i + a) = Matrix.det (Matrix.vandermonde v)

@[simp]

theorem Matrix.det_vandermonde_sub {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) (a : R) : Matrix.det (Matrix.vandermonde fun (i : Fin n) => v i - a) = Matrix.det (Matrix.vandermonde v)

theorem Matrix.eq_zero_of_forall_index_sum_pow_mul_eq_zero {R : Type u_2} [CommRing R] [IsDomain R] {n : ℕ} {f : Fin n → R} {v : Fin n → R} (hf : Function.Injective f) (hfv : ∀ (j : Fin n), (Finset.sum Finset.univ fun (i : Fin n) => f j ^ ↑i * v i) = 0) : v = 0

theorem Matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero {R : Type u_2} [CommRing R] [IsDomain R] {n : ℕ} {f : Fin n → R} {v : Fin n → R} (hf : Function.Injective f) (hfv : ∀ (j : Fin n), (Finset.sum Finset.univ fun (i : Fin n) => v i * f j ^ ↑i) = 0) : v = 0

theorem Matrix.eq_zero_of_forall_pow_sum_mul_pow_eq_zero {R : Type u_2} [CommRing R] [IsDomain R] {n : ℕ} {f : Fin n → R} {v : Fin n → R} (hf : Function.Injective f) (hfv : ∀ (i : Fin n), (Finset.sum Finset.univ fun (j : Fin n) => v j * f j ^ ↑i) = 0) : v = 0

theorem Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) (p : Fin n → Polynomial R) (h_deg : ∀ (i : Fin n), Polynomial.natDegree (p i) ≤ ↑i) : (Matrix.of fun (i j : Fin n) => Polynomial.eval (v i) (p j)) = Matrix.vandermonde v * Matrix.of fun (i j : Fin n) => Polynomial.coeff (p j) ↑i

theorem Matrix.det_eval_matrixOfPolynomials_eq_det_vandermonde {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) (p : Fin n → Polynomial R) (h_deg : ∀ (i : Fin n), Polynomial.natDegree (p i) = ↑i) (h_monic : ∀ (i : Fin n), Polynomial.Monic (p i)) : Matrix.det (Matrix.vandermonde v) = Matrix.det (Matrix.of fun (i j : Fin n) => Polynomial.eval (v i) (p j))