OAI/Combinatorics/MatchingPSD/DeterminantNormalization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PerfectMatchingPSD.convex_posSemidef line 12
2. lemma OAI.PerfectMatchingPSD.hasDerivAt_det_one_add line 16
3. lemma OAI.PerfectMatchingPSD.hasDerivAt_det_add line 34
4. lemma OAI.PerfectMatchingPSD.derivative_nonpos_at_right_max line 47
5. lemma OAI.PerfectMatchingPSD.trace_inv_mul_le_of_det_max line 56
6. lemma OAI.PerfectMatchingPSD.exists_regularized_det_max line 66
7. lemma OAI.PerfectMatchingPSD.trace_mul_nonneg line 103
8. lemma OAI.PerfectMatchingPSD.trace_mul_le_of_le line 112
9. lemma OAI.PerfectMatchingPSD.trace_mul_convexHull_le line 117
10. lemma OAI.PerfectMatchingPSD.exists_normalized_factors line 133