OAI/Analysis/HyperbolicCones/ResolventPositive.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Paper256.complex_symmetric_imaginary_posDef_isUnit line 13
2. theorem OAI.Paper256.resolvent_schur_imaginary_lower_bound line 20
3. theorem OAI.Paper256.resolvent_schur_imaginary_posDef line 52