OAI/LinearAlgebra/MatrixMultiplication/Polynomial/ComplexPolynomialKernelExecution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Polynomial tensor restrictions and exact coefficient extraction.

  1. structure OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution line 16
  2. structure OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Stage line 44
  3. def OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.pack line 71
  4. def OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.step line 79
  5. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.step_rankBound line 132
  6. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.step_auxiliary line 134
  7. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.step_order line 137
  8. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.step_value line 139