OAI/LinearAlgebra/MatrixMultiplication/Polynomial/ComplexPolynomialApproximation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Polynomial tensor restrictions and exact coefficient extraction.

  1. theorem OAI.MatrixMultiplication.Foundation.Tensor.coeff_eq_sum_eval line 20
  2. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.coeff line 35
  3. structure OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation line 60
  4. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.normalized line 71
  5. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.polynomial_eq line 75
  6. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.normalized_constant line 79
  7. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.power_polynomial_eq line 85
  8. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.power line 91
  9. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.rank_power line 117
  10. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.rank_normalized_eval line 137
  11. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.borderRankAtMost line 150