Ranks of the Jacobian and Hessian blocks of matrix multiplication

• Block-triangular minors (sum_min_le_blockRank). Let the rows R g i and columns C g k of a matrix be grouped by g, and order the groups by an injective key. If the entries from a group to a group of smaller key vanish and, within a group g, the entries are those of a totally regular matrix T g, then a block containing P g rows and Q g columns of each group has rank at least ∑ g, min (|P g|, |Q g|): choose min (|P g|, |Q g|) rows and columns of each group; the square submatrix is block triangular (Matrix.BlockTriangular.det) with nonsingular diagonal blocks.
• The derivatives (jacobian_left, jacobian_right, sum_smul_hessian_left_right, ...). The output C i k has derivative [i = i'] B j k in A i' j and [k = k'] A i j in B j k'; the Hessian of ∑ μ (C i k) C i k pairs A i j with B j k through μ (C i k) and has no other nonzero entries.
• The Jacobian blocks (jacobianRows_le_blockRank, jacobianCols_le_blockRank). At a point (A₀, B₀) of totally regular matrices, group the outputs of a heavy row i ∈ H with the inputs A i j (entries B₀ j k), then the outputs of the light rows in a column k with the inputs B j k (entries A₀ i j). An output of a light row has derivative zero in the inputs A i' j of the other rows, so the groups are triangular.
• The Hessian block (chargeJ_le_blockRank_hessian). With μ (C i k) = Λ i k, the cross block of the Hessian is block diagonal over the inner index j, with blocks Λ[rows of A, columns of B] and Λᵀ[rows of B, columns of A], so its rank is at least R_J = chargeJ a b.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.det_submatrix_ne_zero_of_totallyRegular {n : ℕ} {L : Type u_1} [Field L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {T : Matrix (Fin n) (Fin n) L} (hT : TotallyRegular T) {ρ κ : ι → Fin n} (hρ : Function.Injective ρ) (hκ : Function.Injective κ) : (T.submatrix ρ κ).det ≠ 0

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.sum_min_le_blockRank {n : ℕ} {L : Type u_1} [Field L] {G : Type u_2} [Fintype G] [DecidableEq G] (key : G → ℕ) (hkey : Function.Injective key) {m N : ℕ} (M : Matrix (Fin m) (Fin N) L) (Y : Finset (Fin m)) (X : Finset (Fin N)) (R : G → Fin n → Fin m) (C : G → Fin n → Fin N) (T : G → Matrix (Fin n) (Fin n) L) (hT : ∀ (g : G), TotallyRegular (T g)) (P Q : G → Finset (Fin n)) (hR : ∀ (g : G), ∀ i ∈ P g, R g i ∈ Y) (hC : ∀ (g : G), ∀ k ∈ Q g, C g k ∈ X) (hzero : ∀ (g h : G), key h < key g → ∀ i ∈ P g, ∀ k ∈ Q h, M (R g i) (C h k) = 0) (hdiag : ∀ (g : G), ∀ i ∈ P g, ∀ k ∈ Q g, M (R g i) (C g k) = T g i k) : ∑ g : G, min (P g).card (Q g).card ≤ blockRank M Y X

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.matMulRight_ne_matMulLeft {n : ℕ} (j k i j' : Fin n) : matMulRight n j k ≠ matMulLeft n i j'

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.matMulPolynomial_output {n : ℕ} {K : Type u_1} [CommRing K] (i k : Fin n) : matMulPolynomial K n (matMulOutput n i k) = ∑ j : Fin n, MvPolynomial.X (matMulLeft n i j) * MvPolynomial.X (matMulRight n j k)

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.jacobian_left {n : ℕ} {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] [Algebra K L] (a : Fin (n * n + n * n) → L) (i k i' j : Fin n) : Taylor.jacobian (matMulPolynomial K n) a (matMulOutput n i k) (matMulLeft n i' j) = if i = i' then a (matMulRight n j k) else 0

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.jacobian_right {n : ℕ} {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] [Algebra K L] (a : Fin (n * n + n * n) → L) (i k j k' : Fin n) : Taylor.jacobian (matMulPolynomial K n) a (matMulOutput n i k) (matMulRight n j k') = if k = k' then a (matMulLeft n i j) else 0

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.sum_smul_hessian_apply {n : ℕ} {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] [Algebra K L] (μ : Fin (n * n) → L) (a : Fin (n * n + n * n) → L) (x y : Fin (n * n + n * n)) : (∑ o : Fin (n * n), μ o • Taylor.hessian (matMulPolynomial K n o) a) x y = ∑ i : Fin n, ∑ k : Fin n, μ (matMulOutput n i k) * ∑ j : Fin n, ((if y = matMulLeft n i j ∧ x = matMulRight n j k then 1 else 0) + if y = matMulRight n j k ∧ x = matMulLeft n i j then 1 else 0)

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.sum_smul_hessian_left_right {n : ℕ} {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] [Algebra K L] (μ : Fin (n * n) → L) (a : Fin (n * n + n * n) → L) (i j j' k : Fin n) : (∑ o : Fin (n * n), μ o • Taylor.hessian (matMulPolynomial K n o) a) (matMulLeft n i j) (matMulRight n j' k) = if j = j' then μ (matMulOutput n i k) else 0

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.sum_smul_hessian_right_left {n : ℕ} {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] [Algebra K L] (μ : Fin (n * n) → L) (a : Fin (n * n + n * n) → L) (i j j' k : Fin n) : (∑ o : Fin (n * n), μ o • Taylor.hessian (matMulPolynomial K n o) a) (matMulRight n j k) (matMulLeft n i j') = if j = j' then μ (matMulOutput n i k) else 0

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.sum_smul_hessian_left_left {n : ℕ} {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] [Algebra K L] (μ : Fin (n * n) → L) (a : Fin (n * n + n * n) → L) (i j i' j' : Fin n) : (∑ o : Fin (n * n), μ o • Taylor.hessian (matMulPolynomial K n o) a) (matMulLeft n i j) (matMulLeft n i' j') = 0

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.sum_smul_hessian_right_right {n : ℕ} {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] [Algebra K L] (μ : Fin (n * n) → L) (a : Fin (n * n + n * n) → L) (j k j' k' : Fin n) : (∑ o : Fin (n * n), μ o • Taylor.hessian (matMulPolynomial K n o) a) (matMulRight n j k) (matMulRight n j' k') = 0

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.jacobianRows_le_blockRank {n : ℕ} {K : Type u_1} {L : Type u_2} [CommRing K] [Field L] [Algebra K L] {A₀ B₀ : Matrix (Fin n) (Fin n) L} (hA : TotallyRegular A₀) (hB : TotallyRegular B₀) (Y : Finset (Fin (n * n))) (X : Finset (Fin (n * n + n * n))) (cY aX bX : Finset (Fin n × Fin n)) (H : Finset (Fin n)) (hc : ∀ q ∈ cY, matMulOutput n q.1 q.2 ∈ Y) (ha : ∀ q ∈ aX, matMulLeft n q.1 q.2 ∈ X) (hb : ∀ q ∈ bX, matMulRight n q.1 q.2 ∈ X) : Tripartite.jacobianRows cY aX bX H ≤ blockRank (Taylor.jacobian (matMulPolynomial K n) (matMulInput A₀ B₀)) Y X

The row blocks of the Jacobian. At a point (A₀, B₀) of totally regular matrices, the block of the Jacobian with rows Y and columns X has rank at least jacobianRows cY aX bX H.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.jacobianCols_le_blockRank {n : ℕ} {K : Type u_1} {L : Type u_2} [CommRing K] [Field L] [Algebra K L] {A₀ B₀ : Matrix (Fin n) (Fin n) L} (hA : TotallyRegular A₀) (hB : TotallyRegular B₀) (Y : Finset (Fin (n * n))) (X : Finset (Fin (n * n + n * n))) (cY aX bX : Finset (Fin n × Fin n)) (H : Finset (Fin n)) (hc : ∀ q ∈ cY, matMulOutput n q.1 q.2 ∈ Y) (ha : ∀ q ∈ aX, matMulLeft n q.1 q.2 ∈ X) (hb : ∀ q ∈ bX, matMulRight n q.1 q.2 ∈ X) : Tripartite.jacobianCols cY aX bX H ≤ blockRank (Taylor.jacobian (matMulPolynomial K n) (matMulInput A₀ B₀)) Y X

The column blocks of the Jacobian. At a point (A₀, B₀) of totally regular matrices, the block of the Jacobian with rows Y and columns X has rank at least jacobianCols cY aX bX H.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.ArithmeticInternal.chargeJ_le_blockRank_hessian {n : ℕ} {K : Type u_1} {L : Type u_2} [CommRing K] [Field L] [Algebra K L] {Λ : Matrix (Fin n) (Fin n) L} (hΛ : TotallyRegular Λ) (a₀ : Fin (n * n + n * n) → L) (Y : Finset (Fin (n * n + n * n))) (a b : Finset (Fin n × Fin n)) (ha : ∀ (i j : Fin n), (i, j) ∈ a ↔ matMulLeft n i j ∈ Y) (hb : ∀ (j k : Fin n), (j, k) ∈ b ↔ matMulRight n j k ∈ Y) : Tripartite.chargeJ a b ≤ blockRank (∑ o : Fin (n * n), (fun (o : Fin (n * n)) => Λ (finProdFinEquiv.symm o).1 (finProdFinEquiv.symm o).2) o • Taylor.hessian (matMulPolynomial K n o) a₀) Y Yᶜ

The cross block of the Hessian. For a totally regular Λ, let μ (C i k) = Λ i k. If Y holds exactly the inputs A i j with (i, j) ∈ a and B j k with (j, k) ∈ b, the block of the Hessian of ∑ μ o C o with rows Y and columns Yᶜ has rank at least chargeJ a b.