OAI/Probability/StrongRayleigh/MatrixStability.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem336AdditiveD139.quadraticForm_eq_dotProduct line 13
2. lemma OAI.Problem336AdditiveD139.PositiveContractionFinite.isHermitian line 19
3. lemma OAI.Problem336AdditiveD139.PositiveContractionFinite.posSemidef line 24
4. lemma OAI.Problem336AdditiveD139.normSq_sum_eq_dotProduct_re line 34
5. lemma OAI.Problem336AdditiveD139.PositiveContractionFinite.one_sub_posSemidef line 38
6. lemma OAI.Problem336AdditiveD139.positiveContractionFinite_iff_posSemidef line 51
7. lemma OAI.Problem336AdditiveD139.hermitian_pencil_ker_eq_zero line 67
8. lemma OAI.Problem336AdditiveD139.hermitian_pencil_det_ne_zero line 100