OAI/Analysis/NumericalRange/ResolventPositivity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompleteCrouzeix.eigenvalue_mem_numericalRange line 12
2. theorem OAI.CompleteCrouzeix.spectrum_subset_numericalRange line 24
3. lemma OAI.CompleteCrouzeix.isUnit_resolvent_of_not_mem_numericalRange line 36
4. lemma OAI.CompleteCrouzeix.posSemidef_of_unit_quadratic line 43
5. lemma OAI.CompleteCrouzeix.supporting_form_posSemidef line 64
6. theorem OAI.CompleteCrouzeix.supporting_resolvent_posSemidef line 91