OAI/Combinatorics/MatchingCount/Graphs/ThresholdGraph.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Switching.edgeActivity_of_symmetric line 12
  2. theorem OAI.MatchingFPRAS.Switching.erasePair_factor line 19
  3. lemma OAI.MatchingFPRAS.Switching.ultrametric_vertex_charge line 29
  4. lemma OAI.MatchingFPRAS.Switching.ultrametric_pair_charge line 38
  5. lemma OAI.MatchingFPRAS.Switching.pairing_mate_mem line 58
  6. theorem OAI.MatchingFPRAS.Switching.pairing_replace_vertex line 63
  7. theorem OAI.MatchingFPRAS.Switching.pairing_remove_pair line 121
  8. lemma OAI.MatchingFPRAS.Switching.weight_le_pairingCapacity line 222
  9. lemma OAI.MatchingFPRAS.Switching.pairingCapacity_nonneg line 227
  10. theorem OAI.MatchingFPRAS.Switching.capacity_replace_vertex line 233
  11. theorem OAI.MatchingFPRAS.Switching.capacity_remove_pair line 253
  12. def OAI.MatchingFPRAS.Switching.thresholdGraph line 274
  13. lemma OAI.MatchingFPRAS.Switching.strong_walk_reachable line 281
  14. lemma OAI.MatchingFPRAS.Switching.threshold_map_strong line 295
  15. theorem OAI.MatchingFPRAS.Switching.bottleneck_threshold line 304
  16. theorem OAI.MatchingFPRAS.Switching.bottleneck_comm line 333
  17. theorem OAI.MatchingFPRAS.Switching.bottleneck_ultrametric line 347
  18. theorem OAI.MatchingFPRAS.Switching.capacity_charged_remove line 357
  19. theorem OAI.MatchingFPRAS.Switching.capacity_charged_replace line 375
  20. inductive OAI.MatchingFPRAS.Switching.ChargeTrace line 390
  21. lemma OAI.MatchingFPRAS.Switching.ChargeTrace.card_le line 404
  22. lemma OAI.MatchingFPRAS.Switching.even_remove_two line 416
  23. lemma OAI.MatchingFPRAS.Switching.even_replace_one line 430
  24. theorem OAI.MatchingFPRAS.Switching.ChargeTrace.capacity_bound line 437
  25. theorem OAI.MatchingFPRAS.Switching.edgeActivity_le_bottleneck line 464
  26. theorem OAI.MatchingFPRAS.Switching.bottleneck_le_row_bound line 472
  27. theorem OAI.MatchingFPRAS.Switching.bottleneck_eq_of_threshold_iff line 491
  28. def OAI.MatchingFPRAS.Switching.pairVertices line 508
  29. lemma OAI.MatchingFPRAS.Switching.ChargeTrace.trans line 510
  30. theorem OAI.MatchingFPRAS.Switching.charge_remove_list line 524
  31. theorem OAI.MatchingFPRAS.Switching.charge_replace_list line 567