OAI/Combinatorics/MatchingPSD/TensorBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingSmoothing.abs_eigenvalue_le_one_stochastic line 12
  2. lemma OAI.MatchingSmoothing.abs_eigenvalue_le_one_positive_fixed line 26
  3. lemma OAI.MatchingSmoothing.exists_orthogonal_diagonalization_bounded line 61
  4. def OAI.MatchingSmoothing.commonColoringsProdEquiv line 88
  5. lemma OAI.MatchingSmoothing.commonColorings_square line 102
  6. lemma OAI.MatchingSmoothing.pairWeight_nonneg line 109
  7. lemma OAI.MatchingSmoothing.pairWeight_overlap_square_moment line 113
  8. def OAI.MatchingSmoothing.normalizedPairMatrix line 134
  9. lemma OAI.MatchingSmoothing.normalizedPairMatrix_nonneg line 138
  10. lemma OAI.MatchingSmoothing.normalizedPairMatrix_hermitian line 144
  11. lemma OAI.MatchingSmoothing.normalizedPairMatrix_fixed line 152