Documentation

Mathlib.LinearAlgebra.Vandermonde

Vandermonde matrix #

This file defines the vandermonde matrix and gives its determinant.

Main definitions #

Main results #

source
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
Instances For
    source
    @[simp]
    theorem Matrix.vandermonde_apply {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) (i j : Fin n) :
    vandermonde v i j = v i ^ ↑j
    source
    @[simp]
    theorem Matrix.vandermonde_cons {R : Type u_1} [CommRing R] {n : ℕ} (v0 : R) (v : Fin n → R) :
    vandermonde (Fin.cons v0 v) = Fin.cons (fun (j : Fin n.succ) => v0 ^ ↑j) fun (i : Fin n) => Fin.cons 1 fun (j : Fin n) => v i * vandermonde v i j
    source
    theorem Matrix.vandermonde_succ {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n.succ → R) :
    vandermonde v = of Fin.cons (fun (j : Fin n.succ) => v 0 ^ ↑j) fun (i : Fin n) => Fin.cons 1 fun (j : Fin n) => v i.succ * vandermonde (Fin.tail v) i j
    source
    theorem Matrix.vandermonde_mul_vandermonde_transpose {R : Type u_1} [CommRing R] {n : ℕ} (v w : Fin n → R) (i j : Fin n) :
    (vandermonde v * (vandermonde w).transpose) i j = ∑ k : Fin n, (v i * w j) ^ ↑k
    source
    theorem Matrix.vandermonde_transpose_mul_vandermonde {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) (i j : Fin n) :
    ((vandermonde v).transpose * vandermonde v) i j = ∑ k : Fin n, v k ^ (↑i + ↑j)
    source
    theorem Matrix.det_vandermonde {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) :
    (vandermonde v).det = ∏ i : Fin n, ∏ j ∈ Finset.Ioi i, (v j - v i)
    source
    theorem Matrix.det_vandermonde_eq_zero_iff {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} {v : Fin n → R} :
    (vandermonde v).det = 0 ↔ ∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j
    source
    theorem Matrix.det_vandermonde_ne_zero_iff {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} {v : Fin n → R} :
    (vandermonde v).det ≠ 0 ↔ Function.Injective v
    source
    @[simp]
    theorem Matrix.det_vandermonde_add {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) (a : R) :
    (vandermonde fun (i : Fin n) => v i + a).det = (vandermonde v).det
    source
    @[simp]
    theorem Matrix.det_vandermonde_sub {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) (a : R) :
    (vandermonde fun (i : Fin n) => v i - a).det = (vandermonde v).det
    source
    theorem Matrix.eq_zero_of_forall_index_sum_pow_mul_eq_zero {R : Type u_2} [CommRing R] [IsDomain R] {n : ℕ} {f v : Fin n → R} (hf : Function.Injective f) (hfv : ∀ (j : Fin n), ∑ 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_2} [CommRing R] [IsDomain R] {n : ℕ} {f v : Fin n → R} (hf : Function.Injective f) (hfv : ∀ (j : Fin n), ∑ 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_2} [CommRing R] [IsDomain R] {n : ℕ} {f v : Fin n → R} (hf : Function.Injective f) (hfv : ∀ (i : Fin n), ∑ j : Fin n, v j * f j ^ ↑i = 0) :
    v = 0
    source
    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), (p i).natDegree ≤ ↑i) :
    (of fun (i j : Fin n) => Polynomial.eval (v i) (p j)) = vandermonde v * of fun (i j : Fin n) => (p j).coeff ↑i
    source
    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), (p i).natDegree = ↑i) (h_monic : ∀ (i : Fin n), (p i).Monic) :
    (vandermonde v).det = (of fun (i j : Fin n) => Polynomial.eval (v i) (p j)).det