OAI/Combinatorics/MatchingCount/Graphs/PathActivity.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.MatchingFPRAS.Enlargement.vertexLinearOrder line 14
  2. lemma OAI.MatchingFPRAS.Enlargement.terminal_lt_iff line 19
  3. lemma OAI.MatchingFPRAS.Enlargement.real_threshold_eq line 25
  4. theorem OAI.MatchingFPRAS.Enlargement.interval_le_bottleneck line 33
  5. def OAI.MatchingFPRAS.Enlargement.pathActivity line 47
  6. def OAI.MatchingFPRAS.Enlargement.realBottleneck line 50
  7. theorem OAI.MatchingFPRAS.Enlargement.realBottleneck_internal_cap line 54
  8. theorem OAI.MatchingFPRAS.Enlargement.realBottleneck_left_home line 71
  9. theorem OAI.MatchingFPRAS.Enlargement.realBottleneck_right_home line 83
  10. theorem OAI.MatchingFPRAS.Enlargement.realBottleneck_path_lower line 95
  11. def OAI.MatchingFPRAS.Enlargement.leftFactor line 110
  12. def OAI.MatchingFPRAS.Enlargement.rightFactor line 113
  13. def OAI.MatchingFPRAS.Enlargement.neutralFactor line 116
  14. lemma OAI.MatchingFPRAS.Enlargement.leftFactor_eq_potential line 121
  15. lemma OAI.MatchingFPRAS.Enlargement.rightFactor_eq_potential line 128
  16. lemma OAI.MatchingFPRAS.Enlargement.neutralFactor_eq_potential line 135
  17. lemma OAI.MatchingFPRAS.Enlargement.leftFactor_nonneg line 152
  18. lemma OAI.MatchingFPRAS.Enlargement.rightFactor_nonneg line 159
  19. lemma OAI.MatchingFPRAS.Enlargement.neutralFactor_nonneg line 166
  20. theorem OAI.MatchingFPRAS.Enlargement.neutral_local_charge line 176
  21. theorem OAI.MatchingFPRAS.Enlargement.left_local_charge line 219
  22. theorem OAI.MatchingFPRAS.Enlargement.right_local_charge line 236
  23. abbrev OAI.MatchingFPRAS.Enlargement.LogicalEdge line 253
  24. instance OAI.MatchingFPRAS.Enlargement.logicalEdgeLinearOrder line 255
  25. def OAI.MatchingFPRAS.Enlargement.source line 258
  26. def OAI.MatchingFPRAS.Enlargement.target line 260
  27. lemma OAI.MatchingFPRAS.Enlargement.source_ne_target line 263
  28. def OAI.MatchingFPRAS.Enlargement.logicalActivity line 265
  29. lemma OAI.MatchingFPRAS.Enlargement.logical_threshold_eq line 269
  30. theorem OAI.MatchingFPRAS.Enlargement.terminal_bottleneck line 286
  31. def OAI.MatchingFPRAS.Enlargement.enlargedHoles line 303
  32. lemma OAI.MatchingFPRAS.Enlargement.mem_enlargedHoles_left line 309
  33. lemma OAI.MatchingFPRAS.Enlargement.mem_enlargedHoles_right line 315
  34. def OAI.MatchingFPRAS.Enlargement.neutralPairs line 329
  35. def OAI.MatchingFPRAS.Enlargement.consumedPairs line 334
  36. lemma OAI.MatchingFPRAS.Enlargement.tagged_nodup line 341
  37. lemma OAI.MatchingFPRAS.Enlargement.pairVertices_neutral line 355
  38. lemma OAI.MatchingFPRAS.Enlargement.consumed_sources line 363
  39. theorem OAI.MatchingFPRAS.Enlargement.source_lists_nodup line 370
  40. lemma OAI.MatchingFPRAS.Enlargement.mem_neutralPairs line 388
  41. lemma OAI.MatchingFPRAS.Enlargement.mem_consumedPairs line 398