OAI/Combinatorics/PerfectMatching/SeparableCovariance.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatchingEntropy.separableDefect_attains_max line 15
2. theorem OAI.MatchingEntropy.matching_covariance_rank_face line 29
3. theorem OAI.MatchingEntropy.faceCodimension_strict line 55
4. theorem OAI.MatchingEntropy.matching_separable_covariance line 71
5. theorem OAI.MatchingEntropy.matching_covariance_diagonal line 125
6. theorem OAI.MatchingEntropy.separable_max_has_forced line 140