Kernels of matrix blocks

Write ker(M; P, Q) for supportedKernel (M *ᵥ ·) P Q, the vectors supported on the columns P whose image under M vanishes on the rows Q: the kernel of the block M[Q, P].

• Totally regular matrices (card_supportedKernel_mul_pow_le). The block has rank at least min (|P|, |Q|), so |ker(M; P, Q)| · |F| ^ min (|P|, |Q|) ≤ |F| ^ |P|.
• Uniform matrices (sum_card_supportedKernel_mul_pow_le). Summed over all square matrices M, the kernels satisfy (∑ |ker(M; P, Q)|) · |F| ^ min (|P|, |Q|) ≤ 2 |F| ^ (n²) |F| ^ |P|: a nonzero vector d lies in the kernel for at most an |F| ^ -|Q| fraction of the matrices, since each row of Q must be orthogonal to d (card_filter_dotProduct_mul_le).
• Averaging (exists_prod_le_pow). If quantities K t x ≥ 1 average at most 2 q ^ (e t) over x, some x makes ∏ t, K t x ≤ q ^ (∑ t, e t + 2 |T|): the excess exponent log_q (K t x) + 1 - e t is at most K t x / q ^ (e t), so it averages at most 2.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.totallyRegular_transpose {F : Type u_1} [Field F] {m n : ℕ} {M : Matrix (Fin m) (Fin n) F} (hM : TotallyRegular M) : TotallyRegular M.transpose

Transposes of totally regular matrices are totally regular.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.zero_mem_supportedKernel {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n m : ℕ} (M : Matrix (Fin m) (Fin n) F) (P : Finset (Fin n)) (Q : Finset (Fin m)) : 0 ∈ supportedKernel (fun (d : Fin n → F) => M.mulVec d) P Q

Kernels contain the zero vector.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_supportedKernel_pos {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n m : ℕ} (M : Matrix (Fin m) (Fin n) F) (P : Finset (Fin n)) (Q : Finset (Fin m)) : 0 < (supportedKernel (fun (d : Fin n → F) => M.mulVec d) P Q).card

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_supportedKernel_le_pow_sub_blockRank {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n m : ℕ} (M : Matrix (Fin m) (Fin n) F) (P : Finset (Fin n)) (Q : Finset (Fin m)) : (supportedKernel (fun (d : Fin n → F) => M.mulVec d) P Q).card ≤ Fintype.card F ^ (P.card - blockRank M Q P)

ker(M; P, Q) has at most |F| ^ (|P| - rank M[Q, P]) elements.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_supportedKernel_mul_pow_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n m : ℕ} {M : Matrix (Fin m) (Fin n) F} (hM : TotallyRegular M) (P : Finset (Fin n)) (Q : Finset (Fin m)) : (supportedKernel (fun (d : Fin n → F) => M.mulVec d) P Q).card * Fintype.card F ^ min P.card Q.card ≤ Fintype.card F ^ P.card

Kernels of totally regular blocks. |ker(M; P, Q)| · |F| ^ min (|P|, |Q|) ≤ |F| ^ |P|.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_supportedKernel_vecMul_mul_pow_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n m : ℕ} {M : Matrix (Fin n) (Fin m) F} (hM : TotallyRegular M) (P : Finset (Fin n)) (Q : Finset (Fin m)) : (supportedKernel (fun (d : Fin n → F) => Matrix.vecMul d M) P Q).card * Fintype.card F ^ min P.card Q.card ≤ Fintype.card F ^ P.card

Left kernels of totally regular blocks. |ker(Mᵀ; P, Q)| · |F| ^ min (|P|, |Q|) ≤ |F| ^ |P| for the vectors d supported on P with d ᵥ* M vanishing on Q.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_supportedKernel_vecMul_pos {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n m : ℕ} (M : Matrix (Fin n) (Fin m) F) (P : Finset (Fin n)) (Q : Finset (Fin m)) : 0 < (supportedKernel (fun (d : Fin n → F) => Matrix.vecMul d M) P Q).card

Uniform matrices

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_matrix {F : Type u_1} [Fintype F] {n : ℕ} : Fintype.card (Matrix (Fin n) (Fin n) F) = Fintype.card (Fin n → F) ^ n

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_filter_dotProduct_mul_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} {d : Fin n → F} (hd : d ≠ 0) : {r : Fin n → F | r ⬝ᵥ d = 0}.card * Fintype.card F ≤ Fintype.card (Fin n → F)

Vectors orthogonal to a nonzero vector number at most |F| ^ (n - 1).

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_filter_rows_mul_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} {d : Fin n → F} (hd : d ≠ 0) (Q : Finset (Fin n)) : {M : Fin n → Fin n → F | ∀ i ∈ Q, M i ⬝ᵥ d = 0}.card * Fintype.card F ^ Q.card ≤ Fintype.card (Fin n → F) ^ n

Row families orthogonal to a nonzero vector on Q. Families of n rows whose rows in Q are orthogonal to d ≠ 0 number at most |F| ^ (n² - |Q|).

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_filter_mulVec_mul_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} {d : Fin n → F} (hd : d ≠ 0) (Q : Finset (Fin n)) : {M : Matrix (Fin n) (Fin n) F | ∀ i ∈ Q, M.mulVec d i = 0}.card * Fintype.card F ^ Q.card ≤ Fintype.card (Matrix (Fin n) (Fin n) F)

Matrices killing a nonzero vector on Q number at most |F| ^ (n² - |Q|).

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.sum_card_supportedKernel_mul_pow_card_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (P Q : Finset (Fin n)) : (∑ M : Matrix (Fin n) (Fin n) F, (supportedKernel (fun (d : Fin n → F) => M.mulVec d) P Q).card) * Fintype.card F ^ Q.card ≤ Fintype.card (Matrix (Fin n) (Fin n) F) * (Fintype.card F ^ Q.card + Fintype.card F ^ P.card)

Kernels of uniform blocks, exact form. Summed over all square matrices, (∑ |ker(M; P, Q)|) · |F| ^ |Q| ≤ |F| ^ (n²) (|F| ^ |Q| + |F| ^ |P|): the zero vector lies in every kernel, and each of the at most |F| ^ |P| nonzero supported vectors in at most |F| ^ (n² - |Q|) of them.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.sum_card_supportedKernel_mul_pow_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (P Q : Finset (Fin n)) : (∑ M : Matrix (Fin n) (Fin n) F, (supportedKernel (fun (d : Fin n → F) => M.mulVec d) P Q).card) * Fintype.card F ^ min P.card Q.card ≤ 2 * Fintype.card (Matrix (Fin n) (Fin n) F) * Fintype.card F ^ P.card

Kernels of uniform blocks. Summed over all square matrices, (∑ |ker(M; P, Q)|) · |F| ^ min (|P|, |Q|) ≤ 2 |F| ^ (n²) |F| ^ |P|.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.sum_card_supportedKernel_vecMul_mul_pow_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (P Q : Finset (Fin n)) : (∑ M : Matrix (Fin n) (Fin n) F, (supportedKernel (fun (d : Fin n → F) => Matrix.vecMul d M) P Q).card) * Fintype.card F ^ min P.card Q.card ≤ 2 * Fintype.card (Matrix (Fin n) (Fin n) F) * Fintype.card F ^ P.card

Left kernels of uniform blocks. The same bound for ker(Mᵀ; P, Q), the vectors d supported on P with d ᵥ* M vanishing on Q.

Averaging

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.exists_prod_le_pow {X : Type u_2} {T : Type u_3} [Fintype X] [Nonempty X] [Fintype T] {q : ℕ} (hq : 1 < q) (K : T → X → ℕ) (hK : ∀ (t : T) (x : X), 0 < K t x) (e : T → ℕ) (hsum : ∀ (t : T), ∑ x : X, K t x ≤ 2 * Fintype.card X * q ^ e t) : ∃ (x : X), ∏ t : T, K t x ≤ q ^ (∑ t : T, e t + 2 * Fintype.card T)

Averaging. If positive quantities K t x average at most 2 q ^ (e t) over x for every t, some x makes ∏ t, K t x ≤ q ^ (∑ t, e t + 2 |T|).