Vandermonde matrix

This file defines the vandermonde matrix and gives its determinant. For each CommRing R, and function v : Fin n → R the matrix vandermonde v is defined to be Fin n by Fin n matrix V whose ith row is [1, (v i), (v i)^2, ...]. This matrix has determinant equal to the product of v i - v j over all unordered pairs i,j, and therefore is nonsingular if and only if v is injective.

vandermonde v is a special case of two more general matrices we also define. For a type α and functions v w : α → R, we write rectVandermonde v w n for the α × Fin n matrix with ith row [(w i) ^ (n-1), (v i) * (w i)^(n-2), ..., (v i)^(n-1)]. projVandermonde v w = rectVandermonde v w n is the square matrix case, where α = Fin n. The determinant of projVandermonde v w is the product of v j * w i - v i * w j, taken over all pairs i,j with i < j, which gives a similar characterization of when it it nonsingular. Since vandermonde v w = projVandermonde v 1, we can derive most of the API for the former in terms of the latter.

These extensions of Vandermonde matrices arise in the study of complete arcs in finite geometry, coding theory, and representations of uniform matroids over finite fields.

Main definitions

• vandermonde v: a square matrix with the i, jth entry equal to v i ^ j.
• rectVandermonde v w n: an α × Fin n matrix whose i, j-th entry is (v i) ^ j * (w i) ^ (n-1-j).
• projVandermonde v w: a square matrix whose i, j-th entry is (v i) ^ j * (w i) ^ (n-1-j).

Main results

• det_vandermonde: det (vandermonde v) is the product of v j - v i, where (i, j) ranges over the set of pairs with i < j.
• det_projVandermonde: det (projVandermonde v w) is the product of v j * w i - v i * w j, taken over all pairs with i < j.

Implementation notes

We derive the det_vandermonde formula from det_projVandermonde, which is proved using an induction argument involving row operations and division. To circumvent issues with non-invertible elements while still maintaining the generality of rings, we first prove it for fields using the private lemma det_projVandermonde_of_field, and then use an algebraic workaround to generalize to the ring case, stating the strictly more general form as det_projVandermonde.

TODO

Characterize when rectVandermonde v w n has linearly independent rows.

def Matrix.rectVandermonde {R : Type u_1} [CommRing R] {α : Type u_3} (v w : α → R) (n : ℕ) : Matrix α (Fin n) R

A matrix with rows all having the form [b^(n-1), a * b^(n-2), ..., a ^ (n-1)]

Equations

• Matrix.rectVandermonde v w n = Matrix.of fun (i : α) (j : Fin n) => v i ^ ↑j * w i ^ ↑j.rev

def Matrix.projVandermonde {R : Type u_1} [CommRing R] {n : ℕ} (v w : Fin n → R) : Matrix (Fin n) (Fin n) R

A square matrix with rows all having the form [b^(n-1), a * b^(n-2), ..., a ^ (n-1)]

Equations

• Matrix.projVandermonde v w = Matrix.rectVandermonde v w n

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 = Matrix.of fun (i j : Fin n) => v i ^ ↑j

theorem Matrix.vandermonde_eq_projVandermonde {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) : vandermonde v = projVandermonde v 1

theorem Matrix.projVandermonde_apply {R : Type u_1} [CommRing R] {n : ℕ} {v w : Fin n → R} {i j : Fin n} : projVandermonde v w i j = v i ^ ↑j * w i ^ ↑j.rev

We don't mark this as @[simp] because the RHS is not simp-nf, and simplifying the RHS gives a bothersome Nat subtraction.

theorem Matrix.rectVandermonde_apply {R : Type u_1} [CommRing R] {n : ℕ} {α : Type u_3} {v w : α → R} {i : α} {j : Fin n} : rectVandermonde v w n i j = v i ^ ↑j * w i ^ ↑j.rev

@[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

@[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

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

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

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)

theorem Matrix.rectVandermonde_apply_zero_right {R : Type u_1} [CommRing R] {n : ℕ} {α : Type u_3} {v w : α → R} {i : α} (hw : w i = 0) : rectVandermonde v w (n + 1) i = Pi.single (Fin.last n) (v i ^ n)

theorem Matrix.projVandermonde_apply_of_ne_zero {K : Type u_2} [Field K] {n : ℕ} {v w : Fin (n + 1) → K} {i j : Fin (n + 1)} (hw : w i ≠ 0) : projVandermonde v w i j = v i ^ ↑j * w i ^ n / w i ^ ↑j

theorem Matrix.projVandermonde_apply_zero_right {R : Type u_1} [CommRing R] {n : ℕ} {v w : Fin (n + 1) → R} {i : Fin (n + 1)} (hw : w i = 0) : projVandermonde v w i = Pi.single (Fin.last n) (v i ^ n)

theorem Matrix.projVandermonde_comp {R : Type u_1} [CommRing R] {n : ℕ} {v w : Fin n → R} (f : Fin n → Fin n) : projVandermonde (v ∘ f) (w ∘ f) = (projVandermonde v w).submatrix f id

theorem Matrix.projVandermonde_map {R : Type u_1} [CommRing R] {n : ℕ} {R' : Type u_3} [CommRing R'] (φ : R →+* R') (v w : Fin n → R) : (projVandermonde (fun (i : Fin n) => φ (v i)) fun (i : Fin n) => φ (w i)) = φ.mapMatrix (projVandermonde v w)

theorem Matrix.det_projVandermonde {R : Type u_1} [CommRing R] {n : ℕ} (v w : Fin n → R) : (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Finset.Ioi i, (v j * w i - v i * w j)

The formula for the determinant of a projective Vandermonde matrix.

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)

The formula for the determinant of a Vandermonde matrix.

theorem Matrix.det_vandermonde_eq_zero_iff {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] {v : Fin n → R} : (vandermonde v).det = 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] {n : ℕ} [IsDomain R] {v : Fin n → R} : (vandermonde v).det ≠ 0 ↔ Function.Injective v

@[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

@[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

theorem Matrix.eq_zero_of_forall_index_sum_pow_mul_eq_zero {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] {f v : Fin n → R} (hf : Function.Injective f) (hfv : ∀ (j : Fin n), ∑ 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_1} [CommRing R] {n : ℕ} [IsDomain R] {f v : Fin n → R} (hf : Function.Injective f) (hfv : ∀ (j : Fin n), ∑ 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_1} [CommRing R] {n : ℕ} [IsDomain R] {f v : Fin n → R} (hf : Function.Injective f) (hfv : ∀ (i : Fin n), ∑ 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), (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

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