Polynomial tensor restrictions and exact coefficient extraction.

structure MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.CompiledFamily {F : Type u_1} [Field F] {Input : Type u_2} {Output : Type u_3} [Fintype Output] (expressions : Output → Expression F Input) : Type (max (max u_1 u_2) u_3)

A compiled output family with semantic and total operation-count certificates.

• registers : ℕ

  Number of registers allocated to the compiled output family.

• program : Program F Input self.registers

  Program computing the entire indexed output family.

• output : Output → Fin self.registers

  Register holding each compiled output expression.

• correct (inputs : Input → F) (i : Output) : self.program.eval inputs (self.output i) = eval inputs (expressions i)
• cost_eq : self.program.cost = ∑ i : Output, (expressions i).cost

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.compileFinFamily {F : Type u_1} [Field F] {Input : Type u_2} (n : ℕ) (expressions : Fin n → Expression F Input) : CompiledFamily expressions

Compile a family indexed by a standard finite set, appending the individual programs.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.compileFamily {F : Type u_1} [Field F] {Input : Type u_2} {Output : Type u_3} [Fintype Output] (expressions : Output → Expression F Input) : CompiledFamily expressions

Compile an arbitrary finite family after transporting its indices to a standard finite set.

Equations

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