OAI/Combinatorics/MatchingCount/Graphs/SafeSwitch.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.parityPattern_subset_edgeSet line 13
  2. lemma OAI.MatchingFPRAS.Transport.CellDemands.Demand.outside_disjoint_through line 37
  3. lemma OAI.MatchingFPRAS.Transport.CellDemands.Demand.short_error_zero line 45
  4. lemma OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.literal_error line 78
  5. theorem OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.error_load_bound line 93
  6. lemma OAI.MatchingFPRAS.Transport.PatternCode.statewise_swap_bound line 134
  7. theorem OAI.MatchingFPRAS.Transport.PatternCode.weighted_swap_bound line 149
  8. def OAI.MatchingFPRAS.Transport.SafeSwitch line 200
  9. def OAI.MatchingFPRAS.Transport.safeDestinations line 207
  10. def OAI.MatchingFPRAS.Transport.CellPaths.commonInterior line 215
  11. lemma OAI.MatchingFPRAS.Transport.CellPaths.switched_true_common line 218
  12. lemma OAI.MatchingFPRAS.Transport.CellPaths.switched_false_common line 224
  13. lemma OAI.MatchingFPRAS.Transport.CellPaths.safe_switch line 230
  14. def OAI.MatchingFPRAS.Transport.CellDemands.Demand.switchState line 263
  15. lemma OAI.MatchingFPRAS.Transport.CellDemands.Demand.switchState_val line 269
  16. lemma OAI.MatchingFPRAS.Transport.CellDemands.Demand.switchState_safe line 286
  17. lemma OAI.MatchingFPRAS.Transport.CellDemands.Demand.switchChoice_first line 293
  18. theorem OAI.MatchingFPRAS.Transport.CellDemands.Demand.switch_load_bound line 301
  19. def OAI.MatchingFPRAS.Transport.CellDemands.Demand.cellError line 365
  20. def OAI.MatchingFPRAS.Transport.CellDemands.Demand.cellSwitch line 368
  21. def OAI.MatchingFPRAS.Transport.CellDemands.Demand.cellCost line 371
  22. lemma OAI.MatchingFPRAS.Transport.CellDemands.sum_errorDemands line 376
  23. theorem OAI.MatchingFPRAS.Transport.CellDemands.total_cell_demand_load line 409