Arithmetic matrix multiplication: definitions

• matMulPolynomial K n: the outputs C i k = ∑ j, A i j B j k of n × n matrix multiplication as polynomials in the 2 n² inputs, with coefficients in K; it is matMul n evaluated at the variables.

The Jacobian of matrix multiplication at a point (A₀, B₀) sends a change (δA, δB) to δA B₀ + A₀ δB: the entry of the output C i k at the input A i' j is [i = i'] B₀ j k, and at the input B j k' it is [k = k'] A₀ i j. Its blocks between a set Y of outputs and a set X of inputs have rank bounded below by the following sums, in the notation of MatMul.Tripartite.Defs. Here cY holds the pairs (i, k) with C i k ∈ Y, and aX and bX the pairs (i, j) and (j, k) with A i j ∈ X and B j k ∈ X; H is a set of row (or column) vertices.

• Tripartite.jacobianRows cY aX bX H: the sum over the rows i ∈ H of min (#{k : C i k ∈ Y}, #{j : A i j ∈ X}), plus the sum over the columns k of min (#{i ∉ H : C i k ∈ Y}, #{j : B j k ∈ X}).
• Tripartite.jacobianCols cY aX bX H: the mirror image, with rows and columns and the two factors exchanged.

For a split S with placed terminals a, b, c (Tripartite.place):

• Tripartite.jacobianChargeI a b c charges the forward block (outputs outside S, inputs in S) with H the heavy rows, and the backward block (outputs in S, inputs outside S) with H the light rows;
• Tripartite.jacobianChargeK a b c does the same with the columns.

noncomputable def Algebraic.Cutwidth.MultiOutput.matMulPolynomial (K : Type u_1) [CommSemiring K] (n : ℕ) : Fin (n * n) → MvPolynomial (Fin (n * n + n * n)) K

Matrix multiplication as polynomials. The output C i k is the polynomial ∑ j, X (A i j) X (B j k) in the 2 n² inputs: matMul n at the variables.

Equations

• Algebraic.Cutwidth.MultiOutput.matMulPolynomial K n = Algebraic.Cutwidth.MultiOutput.matMul n MvPolynomial.X

def Algebraic.Cutwidth.MultiOutput.Tripartite.jacobianRows {n : ℕ} (cY aX bX : Finset (Fin n × Fin n)) (H : Finset (Fin n)) : ℕ

The Jacobian charge of a block of rows: blocks of rows i ∈ H against the inputs A i j, then blocks of columns k against the inputs B j k, with the rows i ∉ H only.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Cutwidth.MultiOutput.Tripartite.jacobianCols {n : ℕ} (cY aX bX : Finset (Fin n × Fin n)) (H : Finset (Fin n)) : ℕ

The Jacobian charge of a block of columns: blocks of columns k ∈ H against the inputs B j k, then blocks of rows i against the inputs A i j, with the columns k ∉ H only.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Cutwidth.MultiOutput.Tripartite.jacobianChargeI {n : ℕ} (a b c : Finset (Fin n × Fin n)) : ℕ

The row Jacobian charge of a split placing a, b, c: the forward block with the heavy rows and the backward block with the light rows.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Cutwidth.MultiOutput.Tripartite.jacobianChargeK {n : ℕ} (a b c : Finset (Fin n × Fin n)) : ℕ

The column Jacobian charge of a split placing a, b, c: the forward block with the heavy columns and the backward block with the light columns.

Equations

• One or more equations did not get rendered due to their size.