OAI/Combinatorics/MatchingCount/Sampling/EndpointPair.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Transport.CellDemands.componentDifference_cell_bound line 18
  2. lemma OAI.MatchingFPRAS.Transport.CellDemands.sum_componentDifference_bound line 32
  3. lemma OAI.MatchingFPRAS.Transport.CellDemands.sum_demand_eq line 42
  4. theorem OAI.MatchingFPRAS.Transport.CellDemands.variance_cell_demand_bound line 52
  5. lemma OAI.MatchingFPRAS.Transport.label_memberships_le_two line 116
  6. def OAI.MatchingFPRAS.Transport.BagEdge.endpointPair line 127
  7. lemma OAI.MatchingFPRAS.Transport.BagEdge.endpointPair_eq line 132
  8. def OAI.MatchingFPRAS.Transport.BagEdge.verticesColor line 136
  9. lemma OAI.MatchingFPRAS.Transport.BagEdge.verticesColor_injective line 143
  10. lemma OAI.MatchingFPRAS.Transport.bag_edges_card_le line 158
  11. lemma OAI.MatchingFPRAS.Transport.SafeSwitch.weight_ratio line 176
  12. lemma OAI.MatchingFPRAS.Transport.SafeSwitch.gibbs_ratio line 228
  13. lemma OAI.MatchingFPRAS.Transport.SafeSwitch.min_capacity line 235
  14. lemma OAI.MatchingFPRAS.Transport.ColorChange.weight_ratio line 253
  15. lemma OAI.MatchingFPRAS.Transport.ColorChange.min_capacity line 284
  16. lemma OAI.MatchingFPRAS.Transport.color_clamp_comparability line 319
  17. def OAI.MatchingFPRAS.Transport.TwoEdgeSwitch line 343
  18. lemma OAI.MatchingFPRAS.Transport.SafeSwitch.legal line 350
  19. lemma OAI.MatchingFPRAS.Transport.TwoEdgeSwitch.two_le line 356
  20. lemma OAI.MatchingFPRAS.Transport.PM.card_le_vertices line 370
  21. def OAI.MatchingFPRAS.Transport.switchDestinations line 380
  22. def OAI.MatchingFPRAS.Transport.discrepancyComponents line 384
  23. def OAI.MatchingFPRAS.Transport.switchDirichlet line 388
  24. def OAI.MatchingFPRAS.Transport.cycleSquare line 392
  25. def OAI.MatchingFPRAS.Transport.cycleDirichlet line 395
  26. def OAI.MatchingFPRAS.Transport.colorDirichlet line 402
  27. def OAI.MatchingFPRAS.Transport.pairDirichlet line 406
  28. lemma OAI.MatchingFPRAS.Transport.scale_div_lower line 410
  29. lemma OAI.MatchingFPRAS.Transport.switchDirichlet_nonneg line 417
  30. lemma OAI.MatchingFPRAS.Transport.colorDirichlet_nonneg line 427
  31. lemma OAI.MatchingFPRAS.Transport.cycleDirichlet_nonneg line 437