Totally regular matrices

A matrix is totally regular when all of its square submatrices are nonsingular. For a linear map x ↦ M x with a totally regular matrix, any k outputs determine any k inputs once the other inputs are fixed: no small set of outputs is blind to a large set of inputs. This is the property that makes the frontier of a circuit for M wide.

Cauchy matrices M 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 square Cauchy matrices are nonsingular. The explicit family 1 / (i - (N + j)) for 0 ≤ i, j < N is totally regular over every field of characteristic zero (Frontier.totallyRegular_cauchyNat) and over ZMod q for every prime q ≥ 2 N (Frontier.totallyRegular_cauchyZMod).

Main definitions

• Frontier.TotallyRegular M: every square submatrix of M is nonsingular.
• Frontier.cauchy x y: the Cauchy matrix with nodes x and y.

Main results

• Frontier.TotallyRegular.eq_zero: if v is supported on a set of columns C and M v vanishes on a set of rows R with |R| = |C|, then v = 0.
• Frontier.totallyRegular_cauchy: Cauchy matrices are totally regular.

def Complexity.Frontier.TotallyRegular {F : Type u_1} [Field F] {m : Type u_2} {n : Type u_3} (M : Matrix m n F) : Prop

A matrix is totally regular when every square submatrix, on distinct rows and distinct columns, is nonsingular.

Equations

• Complexity.Frontier.TotallyRegular M = ∀ (k : ℕ) (r : Fin k → m) (c : Fin k → n), Function.Injective r → Function.Injective c → (M.submatrix r c).det ≠ 0

theorem Complexity.Frontier.TotallyRegular.eq_zero {F : Type u_1} [Field F] {m : Type u_2} {n : Type u_3} [Fintype n] {M : Matrix m n F} (hM : TotallyRegular M) {R : Finset m} {C : Finset n} (hRC : R.card = C.card) {v : n → F} (hv : ∀ j ∉ C, v j = 0) (hMv : ∀ i ∈ R, M.mulVec v i = 0) : v = 0

Square submatrices are injective. If M is totally regular, v is supported on the columns C, and M v vanishes on the rows R, where |R| = |C|, then v = 0.

Cauchy matrices

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

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

Equations

• Complexity.Frontier.cauchy x y = Matrix.of fun (i : m) (j : n) => (x i - y j)⁻¹

theorem Complexity.Frontier.det_cauchy_ne_zero {F : Type u_1} [Field F] {k : ℕ} (x y : Fin k → F) (hx : Function.Injective x) (hy : Function.Injective y) (hxy : ∀ (i j : Fin k), x i ≠ y j) : (cauchy x y).det ≠ 0

Square Cauchy matrices are nonsingular. If ∑_j v_j / (x_i - y_j) = 0 for all i, the polynomial interpolating the values v_j / w_j at the nodes y_j, where w_j are the nodal weights, vanishes at the k nodes x_i; as its degree is less than k, it is zero, so v = 0.

theorem Complexity.Frontier.totallyRegular_cauchy {F : Type u_1} [Field F] {m : Type u_2} {n : Type u_3} (x : m → F) (y : n → F) (hx : Function.Injective x) (hy : Function.Injective y) (hxy : ∀ (i : m) (j : n), x i ≠ y j) : TotallyRegular (cauchy x y)

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

def Complexity.Frontier.cauchyNat (F : Type u_4) [Field F] (N : ℕ) : Matrix (Fin N) (Fin N) F

The explicit Cauchy matrix M i j = 1 / (i - (N + j)) for 0 ≤ i, j < N.

Equations

• Complexity.Frontier.cauchyNat F N = Complexity.Frontier.cauchy (fun (i : Fin N) => ↑↑i) fun (j : Fin N) => ↑(N + ↑j)

theorem Complexity.Frontier.totallyRegular_cauchyNat {F : Type u_1} [Field F] [CharZero F] (N : ℕ) : TotallyRegular (cauchyNat F N)

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

theorem Complexity.Frontier.totallyRegular_cauchyZMod (q N : ℕ) [Fact (Nat.Prime q)] (hq : 2 * N ≤ q) : TotallyRegular (cauchyNat (ZMod q) N)

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