OAI/Combinatorics/MatchingCount/Sampling/DiscreteLadderSteps.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Transport.discreteLadderSteps line 10
  2. lemma OAI.MatchingFPRAS.Transport.discreteLadderSteps_eq line 13
  3. def OAI.MatchingFPRAS.Transport.finiteLadder line 36
  4. lemma OAI.MatchingFPRAS.Transport.finiteLadder_tv line 48
  5. def OAI.MatchingFPRAS.BottleneckAlgorithm.edge line 76
  6. def OAI.MatchingFPRAS.BottleneckAlgorithm.seed line 78
  7. def OAI.MatchingFPRAS.BottleneckAlgorithm.advance line 80
  8. def OAI.MatchingFPRAS.BottleneckAlgorithm.close line 84
  9. lemma OAI.MatchingFPRAS.BottleneckAlgorithm.close_diag line 88
  10. lemma OAI.MatchingFPRAS.BottleneckAlgorithm.close_one line 91
  11. lemma OAI.MatchingFPRAS.BottleneckAlgorithm.close_mono_step line 102
  12. lemma OAI.MatchingFPRAS.BottleneckAlgorithm.close_mono line 108
  13. lemma OAI.MatchingFPRAS.BottleneckAlgorithm.edge_le_close line 111
  14. lemma OAI.MatchingFPRAS.BottleneckAlgorithm.via_le_close line 117
  15. lemma OAI.MatchingFPRAS.BottleneckAlgorithm.chain_le_close line 122
  16. lemma OAI.MatchingFPRAS.BottleneckAlgorithm.close_le line 141
  17. theorem OAI.MatchingFPRAS.BottleneckAlgorithm.real_close_eq line 168
  18. lemma OAI.MatchingFPRAS.BottleneckAlgorithm.cast_close line 182
  19. theorem OAI.MatchingFPRAS.BottleneckAlgorithm.rational_close_eq line 204