OAI/LinearAlgebra/MatrixMultiplication/Polynomial/ComplexPolynomialControlledKernel.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Polynomial tensor restrictions and exact coefficient extraction.

  1. theorem OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.expanded_mul_coeff_window line 20
  2. theorem OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.expanded_mul_vanishes_of_leading_support line 43
  3. theorem OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.expanded_mul_leading_of_leading_support line 56
  4. abbrev OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.Output line 69
  5. def OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.expandMap line 78
  6. def OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.controlledMap line 82
  7. theorem OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.controlledMap_degree line 91
  8. theorem OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.kernel_expandMap line 107
  9. def OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.mixedStageKernel line 116
  10. def OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.controlledKernel line 125
  11. theorem OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.controlledKernel_factor line 138
  12. theorem OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.controlledKernel_substitution line 168
  13. def OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.controlledLeading line 198
  14. theorem OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.controlledKernel_coefficients line 206
  15. theorem OAI.MatrixMultiplication.Foundation.PolynomialControlledKernel.controlledKernel_rank line 267