Division-free arithmetic programs over a field and their operation counts.

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.sumFin {F : Type u_1} [Field F] {Input : Type u_2} (n : ℕ) : (Fin n → Expression F Input) → Expression F Input

Form a finite sum of arithmetic expressions for the block-recursion construction.

Equations

• One or more equations did not get rendered due to their size.
• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.sumFin 0 x_2 = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.literal 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.eval_sumFin {F : Type u_1} [Field F] {Input : Type u_2} (n : ℕ) (f : Fin n → Expression F Input) (inputs : Input → F) : Expression.eval inputs (sumFin n f) = ∑ i : Fin n, Expression.eval inputs (f i)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.cost_sumFin {F : Type u_1} [Field F] {Input : Type u_2} (n : ℕ) (f : Fin n → Expression F Input) : (sumFin n f).cost = ∑ i : Fin n, (f i).cost + n

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.linear {F : Type u_1} [Field F] {Input : Type u_2} {Term : Type u_3} [Fintype Term] (a : Term → F) (wire : Term → Input) : Expression F Input

Encode a finite linear combination of selected input wires as an arithmetic expression.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.eval_linear {F : Type u_1} [Field F] {Input : Type u_2} {Term : Type u_3} [Fintype Term] (a : Term → F) (wire : Term → Input) (inputs : Input → F) : Expression.eval inputs (linear a wire) = ∑ i : Term, a i * inputs (wire i)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.cost_linear {F : Type u_1} [Field F] {Input : Type u_2} {Term : Type u_3} [Fintype Term] (a : Term → F) (wire : Term → Input) : (linear a wire).cost = 2 * Fintype.card Term

structure MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family (F : Type u_2) (Input : Type u_3) (Output : Type u_4) : Type (max (max u_2 u_3) u_4)

A shared straight-line program with an indexed family of outputs.

• registers : ℕ

  Number of registers allocated to the output family.

• program : Program F Input self.registers

  The program shared by all members of the output family.

• output : Output → Fin self.registers

  Register location of each indexed output.

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval {F : Type u_1} [Field F] {Input : Type u_2} {Output : Type u_4} (p : Family F Input Output) (inputs : Input → F) (o : Output) : F

Evaluate one member of a program's output family.

Equations

• p.eval inputs o = p.program.eval inputs (p.output o)

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost {F : Type u_1} {Input : Type u_2} {Output : Type u_4} (p : Family F Input Output) : ℕ

Arithmetic cost of the shared program, counting each gate once.

Equations

• p.cost = p.program.cost

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.expressions {F : Type u_1} [Field F] {Input : Type u_2} {Output : Type u_4} [Fintype Output] (e : Output → Expression F Input) : Family F Input Output

Compile an indexed family of expressions into a shared output program.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_expressions {F : Type u_1} [Field F] {Input : Type u_2} {Output : Type u_4} [Fintype Output] (e : Output → Expression F Input) (inputs : Input → F) (o : Output) : (expressions e).eval inputs o = Expression.eval inputs (e o)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_expressions {F : Type u_1} [Field F] {Input : Type u_2} {Output : Type u_4} [Fintype Output] (e : Output → Expression F Input) : (expressions e).cost = ∑ o : Output, (e o).cost

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.compose {F : Type u_1} [Field F] {Input : Type u_2} {Mid : Type u_3} {Output : Type u_4} (p : Family F Input Mid) (q : Family F Mid Output) : Family F Input Output

Connect the outputs of one program family to the inputs of another.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_compose {F : Type u_1} [Field F] {Input : Type u_2} {Mid : Type u_3} {Output : Type u_4} (p : Family F Input Mid) (q : Family F Mid Output) (inputs : Input → F) (o : Output) : (p.compose q).eval inputs o = q.eval (p.eval inputs) o

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_compose {F : Type u_1} [Field F] {Input : Type u_2} {Mid : Type u_3} {Output : Type u_4} (p : Family F Input Mid) (q : Family F Mid Output) : (p.compose q).cost = p.cost + q.cost

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.mapInputs {F : Type u_1} {Input : Type u_2} {Output : Type u_4} {NewInput : Type u_5} (f : Input → NewInput) (p : Family F Input Output) : Family F NewInput Output

Relabel the input wires of a program family.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_mapInputs {F : Type u_1} [Field F] {Input : Type u_2} {Output : Type u_4} {NewInput : Type u_5} (f : Input → NewInput) (p : Family F Input Output) (inputs : NewInput → F) (o : Output) : (mapInputs f p).eval inputs o = p.eval (fun (i : Input) => inputs (f i)) o

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_mapInputs {F : Type u_1} {Input : Type u_2} {Output : Type u_4} {NewInput : Type u_5} (f : Input → NewInput) (p : Family F Input Output) : (mapInputs f p).cost = p.cost

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.parallel {F : Type u_1} {Input : Type u_2} {Output : Type u_4} (r : ℕ) : (Fin r → Family F Input Output) → Family F Input (Fin r × Output)

Concatenate a finite family of programs with a common input space.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_parallel {F : Type u_1} [Field F] {Input : Type u_2} {Output : Type u_4} (r : ℕ) (p : Fin r → Family F Input Output) (inputs : Input → F) (o : Fin r × Output) : (parallel r p).eval inputs o = (p o.1).eval inputs o.2

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_parallel {F : Type u_1} {Input : Type u_2} {Output : Type u_4} (r : ℕ) (p : Fin r → Family F Input Output) : (parallel r p).cost = ∑ i : Fin r, (p i).cost

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.copies {F : Type u_1} {Input : Type u_2} {Output : Type u_4} (r : ℕ) (p : Family F Input Output) : Family F (Fin r × Input) (Fin r × Output)

Run independent copies of a program family on separately indexed inputs.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_copies {F : Type u_1} [Field F] {Input : Type u_2} {Output : Type u_4} (r : ℕ) (p : Family F Input Output) (inputs : Fin r × Input → F) (o : Fin r × Output) : (copies r p).eval inputs o = p.eval (fun (x : Input) => inputs (o.1, x)) o.2

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_copies {F : Type u_1} {Input : Type u_2} {Output : Type u_4} (r : ℕ) (p : Family F Input Output) : (copies r p).cost = r * p.cost

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.ofMatrix {F : Type u_1} {m l q : ℕ} (p : MatrixAlgorithm F m l q) : Family F (MatrixInput m l q) (Fin m × Fin q)

View a matrix multiplication algorithm as a family indexed by output positions.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_ofMatrix {F : Type u_1} {m l q : ℕ} (p : MatrixAlgorithm F m l q) : (ofMatrix p).cost = p.cost

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_ofMatrix {F : Type u_1} [Field F] {m l q : ℕ} (p : MatrixAlgorithm F m l q) (hp : p.Correct) (inputs : MatrixInput m l q → F) (o : Fin m × Fin q) : (ofMatrix p).eval inputs o = ∑ j : Fin l, inputs (Sum.inl (o.1, j)) * inputs (Sum.inr (j, o.2))

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.join {n m : ℕ} (i : Fin n) (j : Fin m) : Fin (n * m)

Flatten a pair of finite block and within-block indices.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.join i j = finProdFinEquiv (i, j)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.rank_bilinear_identity {F : Type u_1} [Field F] {n₁ n₂ n₃ r : ℕ} (a : Fin r → Fin n₁ × Fin n₂ → F) (b : Fin r → Fin n₂ × Fin n₃ → F) (c : Fin r → Fin n₃ × Fin n₁ → F) (h : Foundation.Tensor.matrixCoefficients (Fin n₁) (Fin n₂) (Fin n₃) = fun (x : Fin n₁ × Fin n₂) (y : Fin n₂ × Fin n₃) (z : Fin n₃ × Fin n₁) => ∑ q : Fin r, Foundation.Tensor.rankOne (a q) (b q) (c q) x y z) (left : Fin n₁ × Fin n₂ → F) (right : Fin n₂ × Fin n₃ → F) (i : Fin n₁) (k : Fin n₃) : ∑ q : Fin r, (c q (k, i) * ∑ x : Fin n₁ × Fin n₂, a q x * left x) * ∑ y : Fin n₂ × Fin n₃, b q y * right y = ∑ j : Fin n₂, left (i, j) * right (j, k)

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.leftBlock {F : Type u_1} [Field F] {n₁ n₂ r m₁ m₂ : ℕ} (a : Fin r → Fin n₁ × Fin n₂ → F) (A : Matrix (Fin (n₁ * m₁)) (Fin (n₂ * m₂)) F) (q : Fin r) : Matrix (Fin m₁) (Fin m₂) F

The left matrix block obtained from one linear form in a tensor-rank decomposition.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.rightBlock {F : Type u_1} [Field F] {n₂ n₃ r m₂ m₃ : ℕ} (b : Fin r → Fin n₂ × Fin n₃ → F) (B : Matrix (Fin (n₂ * m₂)) (Fin (n₃ * m₃)) F) (q : Fin r) : Matrix (Fin m₂) (Fin m₃) F

The right matrix block obtained from one linear form in a tensor-rank decomposition.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.block_identity {F : Type u_1} [Field F] {n₁ n₂ n₃ r m₁ m₂ m₃ : ℕ} (a : Fin r → Fin n₁ × Fin n₂ → F) (b : Fin r → Fin n₂ × Fin n₃ → F) (c : Fin r → Fin n₃ × Fin n₁ → F) (h : Foundation.Tensor.matrixCoefficients (Fin n₁) (Fin n₂) (Fin n₃) = fun (x : Fin n₁ × Fin n₂) (y : Fin n₂ × Fin n₃) (z : Fin n₃ × Fin n₁) => ∑ q : Fin r, Foundation.Tensor.rankOne (a q) (b q) (c q) x y z) (A : Matrix (Fin (n₁ * m₁)) (Fin (n₂ * m₂)) F) (B : Matrix (Fin (n₂ * m₂)) (Fin (n₃ * m₃)) F) (i : Fin n₁) (k : Fin n₃) (s : Fin m₁) (u : Fin m₃) : ∑ q : Fin r, c q (k, i) * (leftBlock a A q * rightBlock b B q) s u = (A * B) (join i s) (join k u)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.inputExpressions {F : Type u_1} [Field F] {n₁ n₂ n₃ r m₁ m₂ m₃ : ℕ} (a : Fin r → Fin n₁ × Fin n₂ → F) (b : Fin r → Fin n₂ × Fin n₃ → F) : Fin r × MatrixInput m₁ m₂ m₃ → Expression F (MatrixInput (n₁ * m₁) (n₂ * m₂) (n₃ * m₃))

Expressions forming the left and right inputs to all recursive block products.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.inputFamily {F : Type u_1} [Field F] {n₁ n₂ n₃ r m₁ m₂ m₃ : ℕ} (a : Fin r → Fin n₁ × Fin n₂ → F) (b : Fin r → Fin n₂ × Fin n₃ → F) : Family F (MatrixInput (n₁ * m₁) (n₂ * m₂) (n₃ * m₃)) (Fin r × MatrixInput m₁ m₂ m₃)

Compile the input linear forms required by a tensor-rank block decomposition.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.inputFamily_eval {F : Type u_1} [Field F] {n₁ n₂ n₃ r m₁ m₂ m₃ : ℕ} (a : Fin r → Fin n₁ × Fin n₂ → F) (b : Fin r → Fin n₂ × Fin n₃ → F) (A : Matrix (Fin (n₁ * m₁)) (Fin (n₂ * m₂)) F) (B : Matrix (Fin (n₂ * m₂)) (Fin (n₃ * m₃)) F) (q : Fin r) (x : MatrixInput m₁ m₂ m₃) : (inputFamily a b).eval (matrixInputs A B) (q, x) = matrixInputs (leftBlock a A q) (rightBlock b B q) x

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.inputFamily_cost {F : Type u_1} [Field F] {n₁ n₂ n₃ r m₁ m₂ m₃ : ℕ} (a : Fin r → Fin n₁ × Fin n₂ → F) (b : Fin r → Fin n₂ × Fin n₃ → F) : (inputFamily a b).cost = 2 * r * (n₁ * n₂ * m₁ * m₂ + n₂ * n₃ * m₂ * m₃)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.recursiveProducts {F : Type u_1} [Field F] {n₁ n₂ n₃ r m₁ m₂ m₃ : ℕ} (a : Fin r → Fin n₁ × Fin n₂ → F) (b : Fin r → Fin n₂ × Fin n₃ → F) (p : MatrixAlgorithm F m₁ m₂ m₃) : Family F (MatrixInput (n₁ * m₁) (n₂ * m₂) (n₃ * m₃)) (Fin r × Fin m₁ × Fin m₃)

Run the smaller matrix algorithm on each pair of transformed input blocks.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.recursiveProducts_eval {F : Type u_1} [Field F] {n₁ n₂ n₃ r m₁ m₂ m₃ : ℕ} (a : Fin r → Fin n₁ × Fin n₂ → F) (b : Fin r → Fin n₂ × Fin n₃ → F) (p : MatrixAlgorithm F m₁ m₂ m₃) (hp : p.Correct) (A : Matrix (Fin (n₁ * m₁)) (Fin (n₂ * m₂)) F) (B : Matrix (Fin (n₂ * m₂)) (Fin (n₃ * m₃)) F) (q : Fin r) (s : Fin m₁) (u : Fin m₃) : (recursiveProducts a b p).eval (matrixInputs A B) (q, s, u) = (leftBlock a A q * rightBlock b B q) s u

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.recursiveProducts_cost {F : Type u_1} [Field F] {n₁ n₂ n₃ r m₁ m₂ m₃ : ℕ} (a : Fin r → Fin n₁ × Fin n₂ → F) (b : Fin r → Fin n₂ × Fin n₃ → F) (p : MatrixAlgorithm F m₁ m₂ m₃) : (recursiveProducts a b p).cost = 2 * r * (n₁ * n₂ * m₁ * m₂ + n₂ * n₃ * m₂ * m₃) + r * p.cost

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.outputExpressions {F : Type u_1} [Field F] {n₁ n₃ r m₁ m₃ : ℕ} (c : Fin r → Fin n₃ × Fin n₁ → F) : Fin (n₁ * m₁) × Fin (n₃ * m₃) → Expression F (Fin r × Fin m₁ × Fin m₃)

Expressions recombining recursive products into the final matrix entries.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.outputFamily {F : Type u_1} [Field F] {n₁ n₃ r m₁ m₃ : ℕ} (c : Fin r → Fin n₃ × Fin n₁ → F) : Family F (Fin r × Fin m₁ × Fin m₃) (Fin (n₁ * m₁) × Fin (n₃ * m₃))

Compile the output linear forms of the tensor-rank decomposition.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.outputFamily_eval {F : Type u_1} [Field F] {n₁ n₃ r m₁ m₃ : ℕ} (c : Fin r → Fin n₃ × Fin n₁ → F) (inputs : Fin r × Fin m₁ × Fin m₃ → F) (i : Fin n₁) (k : Fin n₃) (s : Fin m₁) (u : Fin m₃) : (outputFamily c).eval inputs (join i s, join k u) = ∑ q : Fin r, c q (k, i) * inputs (q, s, u)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.outputFamily_cost {F : Type u_1} [Field F] {n₁ n₃ r m₁ m₃ : ℕ} (c : Fin r → Fin n₃ × Fin n₁ → F) : (outputFamily c).cost = 2 * r * n₁ * n₃ * m₁ * m₃

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.algorithm {F : Type u_1} [Field F] {n₁ n₂ n₃ r m₁ m₂ m₃ : ℕ} (a : Fin r → Fin n₁ × Fin n₂ → F) (b : Fin r → Fin n₂ × Fin n₃ → F) (c : Fin r → Fin n₃ × Fin n₁ → F) (p : MatrixAlgorithm F m₁ m₂ m₃) : MatrixAlgorithm F (n₁ * m₁) (n₂ * m₂) (n₃ * m₃)

Construct the larger matrix algorithm from a rank decomposition and a smaller algorithm.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.algorithm_correct {F : Type u_1} [Field F] {n₁ n₂ n₃ r m₁ m₂ m₃ : ℕ} (a : Fin r → Fin n₁ × Fin n₂ → F) (b : Fin r → Fin n₂ × Fin n₃ → F) (c : Fin r → Fin n₃ × Fin n₁ → F) (h : Foundation.Tensor.matrixCoefficients (Fin n₁) (Fin n₂) (Fin n₃) = fun (x : Fin n₁ × Fin n₂) (y : Fin n₂ × Fin n₃) (z : Fin n₃ × Fin n₁) => ∑ q : Fin r, Foundation.Tensor.rankOne (a q) (b q) (c q) x y z) (p : MatrixAlgorithm F m₁ m₂ m₃) (hp : p.Correct) : (algorithm a b c p).Correct

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.algorithm_cost {F : Type u_1} [Field F] {n₁ n₂ n₃ r m₁ m₂ m₃ : ℕ} (a : Fin r → Fin n₁ × Fin n₂ → F) (b : Fin r → Fin n₂ × Fin n₃ → F) (c : Fin r → Fin n₃ × Fin n₁ → F) (p : MatrixAlgorithm F m₁ m₂ m₃) : (algorithm a b c p).cost = r * p.cost + 2 * r * (n₁ * n₂ * m₁ * m₂ + n₂ * n₃ * m₂ * m₃ + n₁ * n₃ * m₁ * m₃)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.rank_block_step {F : Type u_1} [Field F] {n₁ n₂ n₃ r m₁ m₂ m₃ : ℕ} (h : (Foundation.Tensor.matrixCoefficients (Fin n₁) (Fin n₂) (Fin n₃)).RankAtMost r) (p : MatrixAlgorithm F m₁ m₂ m₃) (hp : p.Correct) : ∃ (q : MatrixAlgorithm F (n₁ * m₁) (n₂ * m₂) (n₃ * m₃)), q.Correct ∧ q.cost = r * p.cost + 2 * r * (n₁ * n₂ * m₁ * m₂ + n₂ * n₃ * m₂ * m₃ + n₁ * n₃ * m₁ * m₃)