OAI/Analysis/DirectCrouzeix/NumericalRange.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DirectCrouzeix.numericalRange_eq_image line 11
2. theorem OAI.DirectCrouzeix.isCompact_numericalRange line 18
3. theorem OAI.DirectCrouzeix.numericalRange_nonempty line 24
4. theorem OAI.DirectCrouzeix.norm_le_of_mem_numericalRange line 30
5. theorem OAI.DirectCrouzeix.continuous_polynomialValue line 41
6. theorem OAI.DirectCrouzeix.rangeMaximum_attained line 46
7. theorem OAI.DirectCrouzeix.norm_polynomialValue_le_rangeMaximum line 55