OAI/Combinatorics/MatchingCount/Graphs/Height.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Enlargement.row_nonempty line 14
  2. def OAI.MatchingFPRAS.Enlargement.sourceHeight line 18
  3. lemma OAI.MatchingFPRAS.Enlargement.bottleneck_le_sourceHeight line 21
  4. lemma OAI.MatchingFPRAS.Enlargement.one_le_sourceHeight line 25
  5. lemma OAI.MatchingFPRAS.Enlargement.sourceHeight_nonneg line 29
  6. lemma OAI.MatchingFPRAS.Enlargement.sourceHeight_bound line 32
  7. def OAI.MatchingFPRAS.Enlargement.maxSourceHeight line 38
  8. lemma OAI.MatchingFPRAS.Enlargement.sourceHeight_le_max line 41
  9. lemma OAI.MatchingFPRAS.Enlargement.one_le_maxSourceHeight line 44
  10. lemma OAI.MatchingFPRAS.Enlargement.maxSourceHeight_bound line 48
  11. def OAI.MatchingFPRAS.Enlargement.sourceLevels line 52
  12. lemma OAI.MatchingFPRAS.Enlargement.sourceLevels_le line 55
  13. lemma OAI.MatchingFPRAS.Enlargement.maxSourceHeight_lt line 59
  14. abbrev OAI.MatchingFPRAS.Enlargement.SourceVertex line 66
  15. abbrev OAI.MatchingFPRAS.Enlargement.SourceRealEdge line 68
  16. def OAI.MatchingFPRAS.Enlargement.realLeft line 70
  17. def OAI.MatchingFPRAS.Enlargement.realRight line 73
  18. def OAI.MatchingFPRAS.Enlargement.sourceRealB line 76
  19. lemma OAI.MatchingFPRAS.Enlargement.source_profile_strength line 80
  20. lemma OAI.MatchingFPRAS.Enlargement.source_strength_incident_near line 94
  21. lemma OAI.MatchingFPRAS.Enlargement.profile_upper line 117
  22. lemma OAI.MatchingFPRAS.Enlargement.source_strength_le_max line 128
  23. lemma OAI.MatchingFPRAS.Enlargement.sourceRealB_comm line 136
  24. lemma OAI.MatchingFPRAS.Enlargement.sourceRealB_tri line 139
  25. lemma OAI.MatchingFPRAS.Enlargement.sourceRealB_floor line 144
  26. abbrev OAI.MatchingFPRAS.Enlargement.SourceLabel line 147
  27. def OAI.MatchingFPRAS.Enlargement.sourceBags line 150
  28. abbrev OAI.MatchingFPRAS.Enlargement.sourceTree line 155
  29. lemma OAI.MatchingFPRAS.Enlargement.sourceTree_isTree line 158
  30. lemma OAI.MatchingFPRAS.Enlargement.sourceBag_card_le_two line 161
  31. lemma OAI.MatchingFPRAS.Enlargement.sourceBag_tree_adjacent line 170
  32. lemma OAI.MatchingFPRAS.Enlargement.sourceBag_height line 179
  33. def OAI.MatchingFPRAS.Transport.support line 197
  34. lemma OAI.MatchingFPRAS.Transport.mem_support line 202
  35. lemma OAI.MatchingFPRAS.Transport.support_eq_of_matching line 207
  36. abbrev OAI.MatchingFPRAS.Transport.Partial line 217
  37. abbrev OAI.MatchingFPRAS.Transport.Matchings line 219
  38. instance OAI.MatchingFPRAS.Transport.partialFintype line 221
  39. instance OAI.MatchingFPRAS.Transport.matchingsFintype line 223
  40. lemma OAI.MatchingFPRAS.Transport.submatching line 226
  41. lemma OAI.MatchingFPRAS.Transport.support_sdiff_disjoint line 237
  42. def OAI.MatchingFPRAS.Transport.expansionEquiv line 240
  43. def OAI.MatchingFPRAS.Transport.partitionWeight line 267
  44. theorem OAI.MatchingFPRAS.Transport.partition_add line 270
  45. lemma OAI.MatchingFPRAS.Transport.support_empty line 299
  46. def OAI.MatchingFPRAS.Transport.emptyPartial line 302
  47. lemma OAI.MatchingFPRAS.Transport.partial_eq_empty_iff line 305
  48. lemma OAI.MatchingFPRAS.Transport.partitionWeight_nonneg line 309
  49. lemma OAI.MatchingFPRAS.Transport.partitionWeight_mono line 313
  50. lemma OAI.MatchingFPRAS.Transport.pow_mul_linear_le_one line 317
  51. lemma OAI.MatchingFPRAS.Transport.pow_small_le line 332
  52. lemma OAI.MatchingFPRAS.Transport.all_subsets_pow line 338
  53. lemma OAI.MatchingFPRAS.Transport.partial_pow_sum_le line 345
  54. theorem OAI.MatchingFPRAS.Transport.finite_inflation line 355