OAI/Combinatorics/MatchingCount/Sampling/IntervalPattern.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Transport.DemandEncoding.gibbs_bound line 13
  2. theorem OAI.MatchingFPRAS.Transport.IndexedCycle.actual_switch_encoding line 58
  3. theorem OAI.MatchingFPRAS.Transport.IndexedCycle.actual_error_encodings line 91
  4. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeAt_periodic line 151
  5. def OAI.MatchingFPRAS.Transport.IndexedCycle.intervalPattern line 156
  6. def OAI.MatchingFPRAS.Transport.IndexedCycle.parityPattern line 159
  7. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.mem_intervalPattern line 161
  8. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.intervalPattern_union line 166
  9. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.intervalPattern_periodic line 179
  10. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.rotatedPattern line 198
  11. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.arc_through line 206
  12. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.arc_interior line 220
  13. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.cell_piece_interval line 240
  14. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.cell_orientation_parity line 260
  15. def OAI.MatchingFPRAS.Transport.exchange line 302
  16. lemma OAI.MatchingFPRAS.Transport.mem_exchange line 304
  17. lemma OAI.MatchingFPRAS.Transport.exchange_union line 308
  18. lemma OAI.MatchingFPRAS.Transport.exchange_involution line 314
  19. lemma OAI.MatchingFPRAS.Transport.exchange_composition line 320
  20. lemma OAI.MatchingFPRAS.Transport.exchange_multiset line 326
  21. lemma OAI.MatchingFPRAS.Transport.exchange_weight line 336
  22. def OAI.MatchingFPRAS.Transport.ExchangeCompatible line 342
  23. lemma OAI.MatchingFPRAS.Transport.ExchangeCompatible.symm line 346
  24. lemma OAI.MatchingFPRAS.Transport.exchange_matching line 351
  25. def OAI.MatchingFPRAS.Transport.componentEdges line 375
  26. lemma OAI.MatchingFPRAS.Transport.mem_componentEdges line 380
  27. lemma OAI.MatchingFPRAS.Transport.shares_reachable line 385
  28. lemma OAI.MatchingFPRAS.Transport.component_compatible line 392
  29. lemma OAI.MatchingFPRAS.Transport.component_exchange_matching line 401
  30. lemma OAI.MatchingFPRAS.Transport.component_exchange_involution line 406