OAI/LinearAlgebra/MatrixMultiplication/Polynomial/ComplexPolynomialExecutionReindex.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Polynomial tensor restrictions and exact coefficient extraction.

  1. def OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput line 19
  2. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_auxiliary line 56
  3. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_rankBound line 59
  4. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_order line 62
  5. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_leftDegree line 65
  6. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_middleDegree line 68
  7. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_rightDegree line 71
  8. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_leftMap line 74
  9. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_middleMap line 78
  10. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_rightMap line 82
  11. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_value line 86
  12. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_kernel line 93
  13. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_fiberTransform line 104
  14. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_value_preimage line 115
  15. theorem OAI.MatrixMultiplication.Foundation.PolynomialKernelExecution.Execution.reindexOutput_kernel_preimage line 123