OAI/Analysis/Crouzeix/BlockPolynomial.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Block Polynomial.

  1. def OAI.CrouzeixHilbert.blockPolynomialEval line 14
  2. theorem OAI.CrouzeixHilbert.blockPolynomialEval_apply line 41
  3. theorem OAI.CrouzeixHilbert.blockPolynomialEval_smul_constant line 45
  4. theorem OAI.CrouzeixHilbert.blockPolynomialEval_constant line 54
  5. theorem OAI.CrouzeixHilbert.blockPolynomialEval_scalar line 58
  6. theorem OAI.CrouzeixHilbert.blockPolynomialEval_commute line 64
  7. theorem OAI.CrouzeixHilbert.blockPolynomialEval_expansion line 72
  8. theorem OAI.CrouzeixHilbert.Realization.aeval_reduced_denom_isUnit line 81
  9. theorem OAI.CrouzeixHilbert.Realization.aeval_quotient_cancel line 92
  10. theorem OAI.CrouzeixHilbert.Realization.map_ringInverse_equiv line 107
  11. def OAI.CrouzeixHilbert.rationalBaseMatrix line 119
  12. theorem OAI.CrouzeixHilbert.rationalEval_matrix line 122
  13. def OAI.CrouzeixHilbert.blockRationalEval line 131
  14. theorem OAI.CrouzeixHilbert.matrixAmplificationCoordinates_rationalEval line 135
  15. theorem OAI.CrouzeixHilbert.blockRationalEval_denom_cancel line 145