Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.ComplexArithmetic.Programs

Complex arithmetic programs and asymptotic matrix multiplication costs.

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

Relabel register references through the generic gate implementation.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.append {Input : Type u_1} {r : ℕ} (p : Program Input r) {s : ℕ} :
    Program Input s → Program Input (r + s)

    Concatenate complex programs through the generic append implementation.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression (Input : Type u_1) :
      Type u_1

      Complex expressions use the shared field-generic arithmetic syntax.

      Equations
      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression.eval {Input : Type u_1} (inputs : Input → ℂ) :
        Expression Input → ℂ

        Interpret a complex expression with the shared field-generic semantics.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression.cost {Input : Type u_1} :
          Expression Input → ℕ

          Count the arithmetic operations in a complex expression.

          Equations
          Instances For
            source
            @[reducible, inline]
            noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression.compile {Input : Type u_1} (e : Expression Input) :
            Compiled e

            Compile a complex expression with the shared correctness and cost certificates.

            Equations
            Instances For