OAI/LinearAlgebra/MatrixMultiplication/ComplexArithmetic/LowerBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Complex arithmetic programs and asymptotic matrix multiplication costs.

  1. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.eval_eq_constant_or_input_of_cost_eq_zero line 15
  2. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.one_le_cost line 42
  3. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_nonneg line 73
  4. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_bddBelow line 95