OAI/Analysis/HilbertCrouzeix/NumericalRange.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HilbertCrouzeix.norm_le_of_mem_numericalRange line 19
  2. theorem OAI.HilbertCrouzeix.numericalRange_subset_closedBall line 27
  3. theorem OAI.HilbertCrouzeix.numericalClosure_subset_closedBall line 33
  4. theorem OAI.HilbertCrouzeix.isCompact_numericalClosure line 37
  5. theorem OAI.HilbertCrouzeix.numericalRange_nonempty line 42
  6. theorem OAI.HilbertCrouzeix.numericalClosure_nonempty line 48
  7. theorem OAI.HilbertCrouzeix.normSup_empty line 51
  8. theorem OAI.HilbertCrouzeix.isGreatest_normSup line 54
  9. theorem OAI.HilbertCrouzeix.normSup_closure line 61
  10. theorem OAI.HilbertCrouzeix.continuous_matrixPolynomial line 77
  11. theorem OAI.HilbertCrouzeix.polynomial_sup_eq_max line 82
  12. lemma OAI.HilbertCrouzeix.exists_unit_phase line 93
  13. lemma OAI.HilbertCrouzeix.quadratic_cross_im line 109
  14. lemma OAI.HilbertCrouzeix.quadratic_segment_im line 117
  15. lemma OAI.HilbertCrouzeix.unit_segment_ne_zero line 133
  16. lemma OAI.HilbertCrouzeix.zero_mem_numericalRange_of_opposite line 149
  17. theorem OAI.HilbertCrouzeix.convex_numericalRange line 182
  18. theorem OAI.HilbertCrouzeix.convex_numericalClosure line 228