OAI/Combinatorics/MatchingPSD/RepresentationDimension.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingSmoothing.Vertices line 10
  2. def OAI.MatchingSmoothing.firstVertices line 14
  3. lemma OAI.MatchingSmoothing.mem_firstVertices line 17
  4. lemma OAI.MatchingSmoothing.card_firstVertices line 20
  5. def OAI.MatchingSmoothing.pairSwap line 24
  6. lemma OAI.MatchingSmoothing.pairSwap_commute line 27
  7. lemma OAI.MatchingSmoothing.act_pairSwap_commute line 35
  8. lemma OAI.MatchingSmoothing.pairSwap_fixed_outside line 43
  9. lemma OAI.MatchingSmoothing.eigen_weighted_projection line 48
  10. lemma OAI.MatchingSmoothing.next_prescribed_sign line 56
  11. lemma OAI.MatchingSmoothing.exists_negative_projection line 108
  12. lemma OAI.MatchingSmoothing.exists_positive_projection line 121
  13. lemma OAI.MatchingSmoothing.prescribed_sign_vector line 132
  14. lemma OAI.MatchingSmoothing.choose_le_choose_of_le_of_le_compl line 180
  15. lemma OAI.MatchingSmoothing.invariant_high_degree_dimension line 195