Totally regular matrices and Cauchy matrices

A matrix is totally regular when every square submatrix, on distinct rows and distinct columns, is nonsingular; Valiant calls such matrices superregular [Val77]. The definition follows Matrix.IsTotallyUnimodular and Matrix.IsTotallyNonneg. For the linear map x ↦ A x of a totally regular matrix, no small set of outputs is blind to a large set of inputs: a vector supported on a set C of columns that A maps to zero on a set R of at least |C| rows is zero (Matrix.IsTotallyRegular.eq_zero_of_mulVec_eq_zero).

Cauchy matrices A i j = 1 / (x i - y j), with distinct x i, distinct y j and x i ≠ y j, are totally regular: every square submatrix is again a Cauchy matrix, and a square Cauchy matrix is nonsingular (Matrix.det_cauchy_ne_zero). The proof avoids Cauchy's determinant formula: a vector v in the kernel gives a polynomial of degree less than k, the Lagrange interpolant of v j / w j at the nodes y j (where the w j are the nodal weights), that vanishes at the k points x i.

The explicit family 1 / (i - (N + j)) for 0 ≤ i, j < N is totally regular over every field of characteristic zero (Matrix.isTotallyRegular_cauchyNat) and over ZMod q for every prime q ≥ 2 N (Matrix.isTotallyRegular_cauchyNat_zmod).

Main definitions

• Matrix.IsTotallyRegular: every square submatrix is nonsingular.
• Matrix.cauchy: the Cauchy matrix with nodes x and y.
• Matrix.cauchyNat: the Cauchy matrix with nodes 0, ..., N - 1 and N, ..., 2 N - 1.

Main results

• Matrix.isTotallyRegular_iff_fintype: square submatrices indexed by any finite type.
• Matrix.IsTotallyRegular.submatrix, Matrix.IsTotallyRegular.transpose, Matrix.IsTotallyRegular.reindex: closure properties.
• Matrix.IsTotallyRegular.eq_zero_of_mulVec_eq_zero: square submatrices act injectively.
• Matrix.det_cauchy_ne_zero: square Cauchy matrices are nonsingular.
• Matrix.isTotallyRegular_cauchy: Cauchy matrices are totally regular.

References

• L. G. Valiant, Graph-theoretic arguments in low-level complexity

def Matrix.IsTotallyRegular {m : Type u_1} {n : Type u_2} {R : Type u_5} [CommRing R] (A : Matrix m n R) : Prop

A.IsTotallyRegular means that every square submatrix of A, on distinct rows and distinct columns, is nonsingular. These are the superregular matrices of [Val77].

theorem Matrix.isTotallyRegular_iff_fintype {m : Type u_1} {n : Type u_2} {R : Type u_5} [CommRing R] (A : Matrix m n R) : A.IsTotallyRegular ↔ ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n), Function.Injective f → Function.Injective g → (A.submatrix f g).det ≠ 0

A matrix is totally regular exactly when its square submatrices on distinct rows and distinct columns, indexed by any finite type, are nonsingular.

theorem Matrix.IsTotallyRegular.apply_ne_zero {m : Type u_1} {n : Type u_2} {R : Type u_5} [CommRing R] {A : Matrix m n R} (hA : A.IsTotallyRegular) (i : m) (j : n) : A i j ≠ 0

Every entry of a totally regular matrix is nonzero: it is a 1 × 1 submatrix.

theorem Matrix.IsTotallyRegular.submatrix {m : Type u_1} {n : Type u_2} {m' : Type u_3} {n' : Type u_4} {R : Type u_5} [CommRing R] {A : Matrix m n R} (hA : A.IsTotallyRegular) {f : m' → m} {g : n' → n} (hf : Function.Injective f) (hg : Function.Injective g) : (A.submatrix f g).IsTotallyRegular

A submatrix of a totally regular matrix, on distinct rows and distinct columns, is totally regular.

theorem Matrix.IsTotallyRegular.transpose {m : Type u_1} {n : Type u_2} {R : Type u_5} [CommRing R] {A : Matrix m n R} (hA : A.IsTotallyRegular) : A.transpose.IsTotallyRegular

The transpose of a totally regular matrix is totally regular.

theorem Matrix.transpose_isTotallyRegular_iff {m : Type u_1} {n : Type u_2} {R : Type u_5} [CommRing R] (A : Matrix m n R) : A.transpose.IsTotallyRegular ↔ A.IsTotallyRegular

The transpose of A is totally regular exactly when A is.

theorem Matrix.IsTotallyRegular.reindex {m : Type u_1} {n : Type u_2} {m' : Type u_3} {n' : Type u_4} {R : Type u_5} [CommRing R] {A : Matrix m n R} (hA : A.IsTotallyRegular) (em : m ≃ m') (en : n ≃ n') : ((Matrix.reindex em en) A).IsTotallyRegular

Reindexing a totally regular matrix keeps it totally regular.

theorem Matrix.reindex_isTotallyRegular {m : Type u_1} {n : Type u_2} {m' : Type u_3} {n' : Type u_4} {R : Type u_5} [CommRing R] (A : Matrix m n R) (em : m ≃ m') (en : n ≃ n') : ((reindex em en) A).IsTotallyRegular ↔ A.IsTotallyRegular

A reindexing of A along equivalences is totally regular exactly when A is.

theorem Matrix.IsTotallyRegular.eq_zero_of_mulVec_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_5} [CommRing R] {A : Matrix m n R} [Fintype n] [NoZeroDivisors R] (hA : A.IsTotallyRegular) {rows : Finset m} {cols : Finset n} (hcard : cols.card ≤ rows.card) {v : n → R} (hv : ∀ j ∉ cols, v j = 0) (hAv : ∀ i ∈ rows, A.mulVec v i = 0) : v = 0

Square submatrices act injectively. If A is totally regular, v is supported on a set cols of columns, and A v vanishes on a set rows of rows with |cols| ≤ |rows|, then v = 0.

Cauchy matrices

def Matrix.cauchy {m : Type u_1} {n : Type u_2} {F : Type u_6} [Field F] (x : m → F) (y : n → F) : Matrix m n F

The Cauchy matrix with nodes x and y: A i j = 1 / (x i - y j).

@[simp]

theorem Matrix.cauchy_apply {m : Type u_1} {n : Type u_2} {F : Type u_6} [Field F] (x : m → F) (y : n → F) (i : m) (j : n) : cauchy x y i j = (x i - y j)⁻¹

The entry of the Cauchy matrix at (i, j) is (x i - y j)⁻¹.

@[simp]

theorem Matrix.submatrix_cauchy {m : Type u_1} {n : Type u_2} {m' : Type u_3} {n' : Type u_4} {F : Type u_6} [Field F] (x : m → F) (y : n → F) (r : m' → m) (c : n' → n) : (cauchy x y).submatrix r c = cauchy (x ∘ r) (y ∘ c)

A submatrix of a Cauchy matrix is the Cauchy matrix of the restricted nodes.

theorem Matrix.det_cauchy_ne_zero {n : Type u_2} {F : Type u_6} [Field F] [Fintype n] [DecidableEq n] {x y : n → F} (hx : Function.Injective x) (hy : Function.Injective y) (hxy : ∀ (i j : n), x i ≠ y j) : (cauchy x y).det ≠ 0

Square Cauchy matrices are nonsingular. If ∑ j, v j / (x i - y j) = 0 for every i, then the polynomial interpolating v j / w j at the nodes y j, where the w j are the nodal weights, vanishes at the k points x i. Its degree is less than k, so it is zero, and so is v.

theorem Matrix.isTotallyRegular_cauchy {m : Type u_1} {n : Type u_2} {F : Type u_6} [Field F] {x : m → F} {y : n → F} (hx : Function.Injective x) (hy : Function.Injective y) (hxy : ∀ (i : m) (j : n), x i ≠ y j) : (cauchy x y).IsTotallyRegular

Cauchy matrices are totally regular: every square submatrix is again a square Cauchy matrix.

def Matrix.cauchyNat (F : Type u_6) [Field F] (N : ℕ) : Matrix (Fin N) (Fin N) F

The explicit N × N Cauchy matrix A i j = 1 / (i - (N + j)), with nodes 0, ..., N - 1 and N, ..., 2 N - 1.

theorem Matrix.isTotallyRegular_cauchyNat {F : Type u_6} [Field F] [CharZero F] (N : ℕ) : (cauchyNat F N).IsTotallyRegular

The explicit Cauchy matrices are totally regular over fields of characteristic zero.

theorem Matrix.isTotallyRegular_cauchyNat_zmod {q : ℕ} [Fact (Nat.Prime q)] {N : ℕ} (hq : 2 * N ≤ q) : (cauchyNat (ZMod q) N).IsTotallyRegular

The explicit Cauchy matrices are totally regular over ZMod q, for every prime q ≥ 2 N.