OAI/Analysis/Crouzeix/RationalTransfer.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Rational Transfer.

  1. theorem OAI.CrouzeixHilbert.Realization.ratFunc_denom_ne_zero_on_closedDisk line 18
  2. theorem OAI.CrouzeixHilbert.Realization.ratFunc_eval_quotient line 48
  3. theorem OAI.CrouzeixHilbert.Realization.map_ringInverse_of_isUnit line 64
  4. def OAI.CrouzeixHilbert.Realization.pencil line 76
  5. lemma OAI.CrouzeixHilbert.Realization.mapMatrix_scalar line 79
  6. lemma OAI.CrouzeixHilbert.Realization.eval_constantMatrix line 85
  7. lemma OAI.CrouzeixHilbert.Realization.eval_pencil line 90
  8. def OAI.CrouzeixHilbert.Realization.transferDenominator line 95
  9. def OAI.CrouzeixHilbert.Realization.transferNumerator line 97
  10. def OAI.CrouzeixHilbert.Realization.transferRational line 101
  11. lemma OAI.CrouzeixHilbert.Realization.eval_transferDenominator line 105
  12. lemma OAI.CrouzeixHilbert.Realization.eval_transferNumerator line 110
  13. lemma OAI.CrouzeixHilbert.Realization.matrix_inverse_adjugate line 117
  14. theorem OAI.CrouzeixHilbert.Realization.transferRational_eq line 121
  15. def OAI.CrouzeixHilbert.Realization.entryMap line 138
  16. def OAI.CrouzeixHilbert.Realization.Colligation.rational line 150
  17. theorem OAI.CrouzeixHilbert.Realization.Colligation.rational_eq_transfer line 154
  18. theorem OAI.CrouzeixHilbert.Realization.Colligation.norm_rational_le_openDisk line 170
  19. theorem OAI.CrouzeixHilbert.Realization.Colligation.rational_polesOutside line 176
  20. theorem OAI.CrouzeixHilbert.Realization.Colligation.rational_extension line 190
  21. def OAI.CrouzeixHilbert.Realization.conjugateVector line 212
  22. lemma OAI.CrouzeixHilbert.Realization.norm_conjugateVector line 215
  23. lemma OAI.CrouzeixHilbert.Realization.conjugate_apply line 219
  24. lemma OAI.CrouzeixHilbert.Realization.norm_conjugateMatrix_le line 230
  25. theorem OAI.CrouzeixHilbert.Realization.norm_matrix_transpose line 238
  26. def OAI.CrouzeixHilbert.Realization.Colligation.diskExtremal line 249
  27. theorem OAI.CrouzeixHilbert.Realization.Colligation.diskExtremal_function line 252
  28. theorem OAI.CrouzeixHilbert.Realization.Colligation.diskExtremal_polesOutside line 255
  29. theorem OAI.CrouzeixHilbert.Realization.Colligation.diskExtremal_extension line 259