Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.ComplexArithmetic.ProgramComposition

Complex arithmetic programs and asymptotic matrix multiplication costs.

source
@[reducible, inline]
abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.mapInput {Input : Type u_1} {Input' : Type u_2} {Register : Type u_3} (f : Input → Input') :
Gate Input Register → Gate Input' Register

Relabel the inputs of a complex gate through the generic implementation.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.mapSource {Input : Type u_1} {Input' : Type u_2} {Register : Type u_3} (f : Input → Input' ⊕ ℂ) :
    Gate Input Register → Gate Input' Register

    Substitute input wires or scalars in a complex gate.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.mapInput {Input : Type u_1} {Input' : Type u_2} (f : Input → Input') {r : ℕ} :
      Program Input r → Program Input' r

      Relabel complex program inputs through the generic implementation.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.mapSource {Input : Type u_1} {Input' : Type u_2} (f : Input → Input' ⊕ ℂ) {r : ℕ} :
        Program Input r → Program Input' r

        Substitute input wires or scalars throughout a complex program.

        Equations
        Instances For
          source
          @[reducible, inline]
          noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.substitute {Input : Type u_1} {Mid : Type u_2} {r : ℕ} (p : Program Input r) {s : ℕ} (q : Program Mid s) (wires : Mid → Fin r) :
          Substituted p q wires

          Compose complex programs using the generic substitution proof and certificates.

          Equations
          Instances For