OAI/LinearAlgebra/MatrixMultiplication/Polynomial/ComplexPolynomialRestriction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Polynomial tensor restrictions and exact coefficient extraction.

  1. def OAI.MatrixMultiplication.Foundation.Tensor.restrictPolynomial line 19
  2. theorem OAI.MatrixMultiplication.Foundation.Tensor.restrictPolynomial_coeff line 26
  3. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.restrictPolynomial line 34
  4. theorem OAI.MatrixMultiplication.Foundation.Tensor.restrictPolynomial_degree_le line 41
  5. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.ofRankAtMost line 59
  6. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.ofRankAtMost_polynomial line 73
  7. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.restrict line 80
  8. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.restrict_polynomial line 97