OAI/Combinatorics/MatchingPSD/ColoringCounts.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingSmoothing.histogram line 11
  2. lemma OAI.MatchingSmoothing.sum_histogram line 14
  3. abbrev OAI.MatchingSmoothing.Colorings line 20
  4. instance OAI.MatchingSmoothing.coloringsFintype line 23
  5. def OAI.MatchingSmoothing.fiberEquivOfHistogram line 26
  6. def OAI.MatchingSmoothing.permOfHistogram line 30
  7. lemma OAI.MatchingSmoothing.permOfHistogram_spec line 35
  8. lemma OAI.MatchingSmoothing.histogram_comp_perm line 39
  9. def OAI.MatchingSmoothing.fiberPermEquiv line 48
  10. lemma OAI.MatchingSmoothing.card_colorings_mul_factorials line 67
  11. lemma OAI.MatchingSmoothing.card_colorings_eq_multinomial line 87
  12. lemma OAI.MatchingSmoothing.card_perm_color_fiber line 94
  13. lemma OAI.MatchingSmoothing.sum_perm_comp line 104
  14. lemma OAI.MatchingSmoothing.mean_perm_comp line 124
  15. def OAI.MatchingSmoothing.pairConstant line 137
  16. instance OAI.MatchingSmoothing.pairConstantDecidable line 139
  17. def OAI.MatchingSmoothing.duplicateColoring line 142
  18. def OAI.MatchingSmoothing.pairConstantEquiv line 144
  19. def OAI.MatchingSmoothing.spliceColoring line 155
  20. lemma OAI.MatchingSmoothing.histogram_spliceColoring line 159
  21. lemma OAI.MatchingSmoothing.histogram_duplicateColoring line 177
  22. lemma OAI.MatchingSmoothing.card_colorings_double_ge_square line 186
  23. def OAI.MatchingSmoothing.constantColoringsEquiv line 206
  24. lemma OAI.MatchingSmoothing.sum_indicator_card line 230
  25. lemma OAI.MatchingSmoothing.sum_pairConstant line 237
  26. lemma OAI.MatchingSmoothing.pairConstant_perm_sum_bound line 247
  27. lemma OAI.MatchingSmoothing.sum_le_card_mul_of_fiber_bound line 271
  28. def OAI.MatchingSmoothing.boundedHistogram line 295
  29. lemma OAI.MatchingSmoothing.boundedHistogram_eq_iff line 300
  30. lemma OAI.MatchingSmoothing.common_pairColorings_moment line 306