OAI/Analysis/NumericalRange/UnitaryRealization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CompleteCrouzeix.exists_unitary_intertwining line 55
  2. theorem OAI.CompleteCrouzeix.exists_unitary_of_row_gram line 88
  3. theorem OAI.CompleteCrouzeix.exists_unitary_matrix_of_gram line 107
  4. theorem OAI.CompleteCrouzeix.exists_unitary_row_realization line 141
  5. lemma OAI.CompleteCrouzeix.block_one₁₁ line 168
  6. lemma OAI.CompleteCrouzeix.block_one₂₂ line 174
  7. lemma OAI.CompleteCrouzeix.norm_le_one_of_star_mul_le line 180
  8. lemma OAI.CompleteCrouzeix.block_unitary_contractions line 186
  9. def OAI.CompleteCrouzeix.transfer line 204
  10. theorem OAI.CompleteCrouzeix.transfer_contraction line 207
  11. lemma OAI.CompleteCrouzeix.meromorphic_matrix_det line 266
  12. lemma OAI.CompleteCrouzeix.meromorphic_matrix_adjugate line 274
  13. lemma OAI.CompleteCrouzeix.meromorphic_matrix_inverse line 285
  14. lemma OAI.CompleteCrouzeix.meromorphic_order_nonneg_of_disk_bound line 295
  15. lemma OAI.CompleteCrouzeix.bounded_meromorphic_disk_extension line 315