Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.Arithmetic.Complexity

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

source
@[simp]
theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.eval_step_zero {F : Type u_1} {Input : Type u_2} [Field F] {r : ℕ} (p : Program F Input r) (g : Gate F Input (Fin r)) (inputs : Input → F) :
(p.step g).eval inputs 0 = Gate.eval inputs (p.eval inputs) g
source
@[simp]
theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.eval_step_succ {F : Type u_1} {Input : Type u_2} [Field F] {r : ℕ} (p : Program F Input r) (g : Gate F Input (Fin r)) (inputs : Input → F) (i : Fin r) :
(p.step g).eval inputs i.succ = p.eval inputs i
source
@[simp]
theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.cost_step {F : Type u_1} {Input : Type u_2} {r : ℕ} (p : Program F Input r) (g : Gate F Input (Fin r)) :
(p.step g).cost = p.cost + g.cost
source
theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.correct_iff_entries {F : Type u_1} [Field F] {a b c : ℕ} (P : MatrixAlgorithm F a b c) :
P.Correct ↔ ∀ (A : Matrix (Fin a) (Fin b) F) (B : Matrix (Fin b) (Fin c) F) (i : Fin a) (k : Fin c), P.program.eval (matrixInputs A B) (P.output i k) = ∑ j : Fin b, A i j * B j k
source
def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.scalarAlgorithm (F : Type u_1) :
MatrixAlgorithm F 1 1 1

Multiply two scalar inputs using one multiplication gate.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.scalarAlgorithm_correct (F : Type u_1) [Field F] :
    (scalarAlgorithm F).Correct
    source
    @[simp]
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.scalarAlgorithm_cost (F : Type u_1) :
    (scalarAlgorithm F).cost = 1
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.one_le_innerSize {n : ℕ} (hn : 1 ≤ n) (k : ℝ) :
    1 ≤ innerSize n k
    source
    @[simp]
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.innerSize_zero (n : ℕ) :
    innerSize n 0 = 1
    source
    @[simp]
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.innerSize_one (n : ℕ) :
    innerSize n 1 = n
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.innerSize_mono {n : ℕ} (hn : 1 ≤ n) {k l : ℝ} (hkl : k ≤ l) :
    innerSize n k ≤ innerSize n l
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.innerSize_le_pow {a b n t : ℕ} {k : ℝ} (hk : 0 ≤ k) (hn : n ≤ a ^ t) (hab : ↑a ^ k ≤ ↑b) :
    innerSize n k ≤ b ^ t
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.innerSize_cast_le {n : ℕ} (hn : 1 ≤ n) {k : ℝ} (hk : 0 ≤ k) :
    ↑(innerSize n k) ≤ 2 * ↑n ^ k