OAI/Computability/MatchingCount/OracleBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryMatching.DenseOracle.total line 11
2. lemma OAI.BinaryMatching.DenseOracle.entry_le_total line 13
3. lemma OAI.BinaryMatching.DenseOracle.source_le_total line 17
4. lemma OAI.BinaryMatching.DenseOracle.push_total_le line 20
5. lemma OAI.BinaryMatching.DenseOracle.contract_total_le line 33
6. lemma OAI.BinaryMatching.DenseOracle.feasible_abs_bound line 38
7. lemma OAI.BinaryMatching.DenseOracle.flow_abs_bound line 47
8. lemma OAI.BinaryMatching.DenseOracle.path_length_bound line 52
9. def OAI.BinaryMatching.DenseOracle.calls line 60
10. lemma OAI.BinaryMatching.DenseOracle.calls_bound line 71
11. lemma OAI.BinaryMatching.DenseOracle.initial_total_bound line 109