Complex arithmetic interfaces specialized from the shared field-generic implementation.

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.sumFin {Input : Type u_1} (n : ℕ) : (Fin n → Expression Input) → Expression 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.

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

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

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.linear {Input : Type u_1} {Term : Type u_2} [Fintype Term] (a : Term → ℂ) (wire : Term → Input) : Expression 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.Foundation.Arithmetic.RecursiveBlock.LinearExpression.eval_linear {Input : Type u_1} {Term : Type u_2} [Fintype Term] (a : Term → ℂ) (wire : Term → Input) (inputs : Input → ℂ) : Expression.eval inputs (linear a wire) = ∑ i : Term, a i * inputs (wire i)

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

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family (Input : Type u_1) (Output : Type u_2) : Type (max u_1 u_2)

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

Equations

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

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval {Input : Type u_1} {Output : Type u_3} (p : Family Input Output) (inputs : Input → ℂ) (o : Output) : ℂ

Evaluate one member of a program's output family.

Equations

• p.eval inputs o = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval p inputs o

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost {Input : Type u_1} {Output : Type u_3} (p : Family Input Output) : ℕ

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

Equations

• p.cost = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost p

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.expressions {Input : Type u_1} {Output : Type u_3} [Fintype Output] (e : Output → Expression Input) : Family 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.Foundation.Arithmetic.RecursiveBlock.Family.eval_expressions {Input : Type u_1} {Output : Type u_3} [Fintype Output] (e : Output → Expression Input) (inputs : Input → ℂ) (o : Output) : (expressions e).eval inputs o = Expression.eval inputs (e o)

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

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.compose {Input : Type u_1} {Mid : Type u_2} {Output : Type u_3} (p : Family Input Mid) (q : Family Mid Output) : Family Input Output

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

Equations

• p.compose q = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.compose p q

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

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

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.mapInputs {Input : Type u_1} {Output : Type u_3} {NewInput : Type u_4} (f : Input → NewInput) (p : Family Input Output) : Family 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.Foundation.Arithmetic.RecursiveBlock.Family.eval_mapInputs {Input : Type u_1} {Output : Type u_3} {NewInput : Type u_4} (f : Input → NewInput) (p : Family Input Output) (inputs : NewInput → ℂ) (o : Output) : (mapInputs f p).eval inputs o = p.eval (fun (i : Input) => inputs (f i)) o

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

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.parallel {Input : Type u_1} {Output : Type u_3} (r : ℕ) : (Fin r → Family Input Output) → Family 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.Foundation.Arithmetic.RecursiveBlock.Family.eval_parallel {Input : Type u_1} {Output : Type u_3} (r : ℕ) (p : Fin r → Family Input Output) (inputs : Input → ℂ) (o : Fin r × Output) : (parallel r p).eval inputs o = (p o.1).eval inputs o.2

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

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.copies {Input : Type u_1} {Output : Type u_3} (r : ℕ) (p : Family Input Output) : Family (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.Foundation.Arithmetic.RecursiveBlock.Family.eval_copies {Input : Type u_1} {Output : Type u_3} (r : ℕ) (p : Family Input Output) (inputs : Fin r × Input → ℂ) (o : Fin r × Output) : (copies r p).eval inputs o = p.eval (fun (x : Input) => inputs (o.1, x)) o.2

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

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.ofMatrix {m : ℕ} (p : MatrixAlgorithm m) : Family (MatrixInput m) (Fin m × Fin m)

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.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost_ofMatrix {m : ℕ} (p : MatrixAlgorithm m) : (ofMatrix p).cost = p.cost

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval_ofMatrix {m : ℕ} (p : MatrixAlgorithm m) (hp : p.Correct) (inputs : MatrixInput m → ℂ) (o : Fin m × Fin m) : (ofMatrix p).eval inputs o = ∑ j : Fin m, inputs (Sum.inl (o.1, j)) * inputs (Sum.inr (j, o.2))

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.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.Foundation.Arithmetic.RecursiveBlock.join i j = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.join i j

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.rank_bilinear_identity {n r : ℕ} (a b c : Fin r → Fin n × Fin n → ℂ) (h : Tensor.matrixMultiplication n n n = fun (x y z : Fin n × Fin n) => ∑ q : Fin r, Tensor.rankOne (a q) (b q) (c q) x y z) (left right : Fin n × Fin n → ℂ) (i 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)

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.leftBlock {n r m : ℕ} (a : Fin r → Fin n × Fin n → ℂ) (A : Matrix (Fin (n * m)) (Fin (n * m)) ℂ) (q : Fin r) : Matrix (Fin m) (Fin m) ℂ

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.

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.rightBlock {n r m : ℕ} (b : Fin r → Fin n × Fin n → ℂ) (B : Matrix (Fin (n * m)) (Fin (n * m)) ℂ) (q : Fin r) : Matrix (Fin m) (Fin m) ℂ

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.Foundation.Arithmetic.RecursiveBlock.block_identity {n r m : ℕ} (a b c : Fin r → Fin n × Fin n → ℂ) (h : Tensor.matrixMultiplication n n n = fun (x y z : Fin n × Fin n) => ∑ q : Fin r, Tensor.rankOne (a q) (b q) (c q) x y z) (A B : Matrix (Fin (n * m)) (Fin (n * m)) ℂ) (i k : Fin n) (s 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)

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.inputExpressions {n r m : ℕ} (a b : Fin r → Fin n × Fin n → ℂ) : Fin r × MatrixInput m → Expression (MatrixInput (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.

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.inputFamily {n r m : ℕ} (a b : Fin r → Fin n × Fin n → ℂ) : Family (MatrixInput (n * m)) (Fin r × MatrixInput 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.Foundation.Arithmetic.RecursiveBlock.inputFamily_eval {n r m : ℕ} (a b : Fin r → Fin n × Fin n → ℂ) (A B : Matrix (Fin (n * m)) (Fin (n * m)) ℂ) (q : Fin r) (x : MatrixInput m) : (inputFamily a b).eval (MatrixMultiplication.Arithmetic.matrixInputs A B) (q, x) = MatrixMultiplication.Arithmetic.matrixInputs (leftBlock a A q) (rightBlock b B q) x

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.inputFamily_cost {n r m : ℕ} (a b : Fin r → Fin n × Fin n → ℂ) : (inputFamily a b).cost = 4 * r * n ^ 2 * m ^ 2

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.recursiveProducts {n r m : ℕ} (a b : Fin r → Fin n × Fin n → ℂ) (p : MatrixAlgorithm m) : Family (MatrixInput (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.Foundation.Arithmetic.RecursiveBlock.recursiveProducts_eval {n r m : ℕ} (a b : Fin r → Fin n × Fin n → ℂ) (p : MatrixAlgorithm m) (hp : p.Correct) (A B : Matrix (Fin (n * m)) (Fin (n * m)) ℂ) (q : Fin r) (s u : Fin m) : (recursiveProducts a b p).eval (MatrixMultiplication.Arithmetic.matrixInputs A B) (q, s, u) = (leftBlock a A q * rightBlock b B q) s u

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.recursiveProducts_cost {n r m : ℕ} (a b : Fin r → Fin n × Fin n → ℂ) (p : MatrixAlgorithm m) : (recursiveProducts a b p).cost = 4 * r * n ^ 2 * m ^ 2 + r * p.cost

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.outputExpressions {n r m : ℕ} (c : Fin r → Fin n × Fin n → ℂ) : Fin (n * m) × Fin (n * m) → Expression (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.

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.outputFamily {n r m : ℕ} (c : Fin r → Fin n × Fin n → ℂ) : Family (Fin r × Fin m × Fin m) (Fin (n * m) × Fin (n * m))

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

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.outputFamily c = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.outputFamily c

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.outputFamily_eval {n r m : ℕ} (c : Fin r → Fin n × Fin n → ℂ) (inputs : Fin r × Fin m × Fin m → ℂ) (i k : Fin n) (s 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.Foundation.Arithmetic.RecursiveBlock.outputFamily_cost {n r m : ℕ} (c : Fin r → Fin n × Fin n → ℂ) : (outputFamily c).cost = 2 * r * n ^ 2 * m ^ 2

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.algorithm {n r m : ℕ} (a b c : Fin r → Fin n × Fin n → ℂ) (p : MatrixAlgorithm m) : MatrixAlgorithm (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.Foundation.Arithmetic.RecursiveBlock.algorithm_correct {n r m : ℕ} (a b c : Fin r → Fin n × Fin n → ℂ) (h : Tensor.matrixMultiplication n n n = fun (x y z : Fin n × Fin n) => ∑ q : Fin r, Tensor.rankOne (a q) (b q) (c q) x y z) (p : MatrixAlgorithm m) (hp : p.Correct) : (algorithm a b c p).Correct

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.algorithm_cost {n r m : ℕ} (a b c : Fin r → Fin n × Fin n → ℂ) (p : MatrixAlgorithm m) : (algorithm a b c p).cost = r * p.cost + 6 * r * n ^ 2 * m ^ 2

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.rank_block_step {n r m : ℕ} (h : (Tensor.matrixMultiplication n n n).RankAtMost r) (p : MatrixAlgorithm m) (hp : p.Correct) : ∃ (q : MatrixAlgorithm (n * m)), q.Correct ∧ q.cost = r * p.cost + 6 * r * n ^ 2 * m ^ 2