OAI/Combinatorics/MatchingPSD/TableCoordinates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingSmoothing.tableCoordinate_symm line 12
  2. lemma OAI.MatchingSmoothing.tableCoordinate_row_sum line 21
  3. lemma OAI.MatchingSmoothing.tableCoordinate_diagonal line 34
  4. def OAI.MatchingSmoothing.crossPair line 47
  5. def OAI.MatchingSmoothing.crossCoordinate line 48
  6. lemma OAI.MatchingSmoothing.tableCoordinate_offdiag_low line 51
  7. lemma OAI.MatchingSmoothing.tableCoordinate_three_affine line 63
  8. lemma OAI.MatchingSmoothing.colorAverage_cross_lowDegree line 78
  9. lemma OAI.MatchingSmoothing.colorAverage_polynomial line 84
  10. lemma OAI.MatchingSmoothing.tableCoordinate_relabel line 95
  11. lemma OAI.MatchingSmoothing.three_order_indicator line 104
  12. lemma OAI.MatchingSmoothing.standard_tableCoordinate line 111
  13. lemma OAI.MatchingSmoothing.tableCoordinate_eq_table line 130
  14. lemma OAI.MatchingSmoothing.crossCoordinate_eq_table line 139