OAI/Analysis/Crouzeix/EndpointInterpolation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Endpoint Interpolation.

  1. theorem OAI.CrouzeixHilbert.aeval_transferDenominator_isUnit line 16
  2. theorem OAI.CrouzeixHilbert.transferDenominator_ne_zero line 34
  3. theorem OAI.CrouzeixHilbert.leftTensor_isUnit line 41
  4. theorem OAI.CrouzeixHilbert.blockPolynomialEval_pencil_transpose line 49
  5. theorem OAI.CrouzeixHilbert.blockPolynomialEval_adjugate_pencil line 55
  6. theorem OAI.CrouzeixHilbert.blockPolynomialEval_transferNumerator_transpose line 63
  7. theorem OAI.CrouzeixHilbert.rational_transfer_interpolates line 73