OAI/Combinatorics/MatchingCount/Sampling/ComponentOrder.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Transport.componentOrder line 15
  2. def OAI.MatchingFPRAS.Transport.componentPrefix line 19
  3. lemma OAI.MatchingFPRAS.Transport.mem_componentPrefix line 25
  4. lemma OAI.MatchingFPRAS.Transport.componentPrefix_zero line 33
  5. lemma OAI.MatchingFPRAS.Transport.componentPrefix_succ line 38
  6. lemma OAI.MatchingFPRAS.Transport.componentPrefix_full line 54
  7. lemma OAI.MatchingFPRAS.Transport.componentPrefix_disjoint line 68
  8. lemma OAI.MatchingFPRAS.Transport.componentPrefix_compatible line 85
  9. lemma OAI.MatchingFPRAS.Transport.exchange_empty line 97
  10. lemma OAI.MatchingFPRAS.Transport.exchange_all line 100
  11. lemma OAI.MatchingFPRAS.Transport.exchange_disjoint_composition line 105
  12. lemma OAI.MatchingFPRAS.Transport.componentPrefix_step line 115
  13. def OAI.MatchingFPRAS.Transport.prefixPair line 132
  14. lemma OAI.MatchingFPRAS.Transport.prefixPair_union line 139
  15. lemma OAI.MatchingFPRAS.Transport.prefixPair_involutive line 144
  16. lemma OAI.MatchingFPRAS.Transport.prefixPair_zero line 158
  17. lemma OAI.MatchingFPRAS.Transport.componentPrefix_eq_full line 162
  18. lemma OAI.MatchingFPRAS.Transport.prefixPair_full line 177
  19. def OAI.MatchingFPRAS.Transport.componentAt line 186
  20. lemma OAI.MatchingFPRAS.Transport.componentAt_compatible line 190
  21. def OAI.MatchingFPRAS.Transport.componentPair line 199
  22. lemma OAI.MatchingFPRAS.Transport.prefixPair_step line 206
  23. lemma OAI.MatchingFPRAS.Transport.prefixPair_gibbs line 228
  24. def OAI.MatchingFPRAS.Transport.componentDifference line 234
  25. lemma OAI.MatchingFPRAS.Transport.prefix_difference_sum line 238
  26. lemma OAI.MatchingFPRAS.Transport.canonical_path_square line 249
  27. lemma OAI.MatchingFPRAS.Transport.sum_prefixPair line 263
  28. theorem OAI.MatchingFPRAS.Transport.cycle_demand_variance line 276
  29. def OAI.MatchingFPRAS.Transport.ColorChange line 318
  30. def OAI.MatchingFPRAS.Transport.colorDestinations line 321
  31. lemma OAI.MatchingFPRAS.Transport.matching_inter_parallel line 327
  32. lemma OAI.MatchingFPRAS.Transport.parallel_exchange_color line 344
  33. lemma OAI.MatchingFPRAS.Transport.CellDemands.Demand.cellCost_nonneg line 377
  34. lemma OAI.MatchingFPRAS.Transport.CellDemands.Demand.cellCost_eq line 381
  35. def OAI.MatchingFPRAS.Transport.CellDemands.longCellCost line 388
  36. lemma OAI.MatchingFPRAS.Transport.CellDemands.longCellCost_nonneg line 393
  37. def OAI.MatchingFPRAS.Transport.CellDemands.colorCost line 397
  38. lemma OAI.MatchingFPRAS.Transport.CellDemands.colorCost_nonneg line 401
  39. theorem OAI.MatchingFPRAS.Transport.CellDemands.component_cell_bound line 405
  40. lemma OAI.arbitrary_sigma_sum line 446