OAI/Combinatorics/MatchingCount/Sampling/DPEnvelope.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.UnitRefresh.Materialized.RowBound line 12
2. def OAI.MatchingFPRAS.UnitRefresh.Materialized.mergeEnvelope line 14
3. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.mergeEnvelope_pos line 17
4. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.mergeEnvelope_prod line 28
5. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.entry_rowBound line 46
6. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.update_rowBound line 78
7. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.sharedCount_le_card line 90
8. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.run_envelope line 94
9. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.run_entry_le line 125
10. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.pairingCount_pow_bound line 132
11. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.initial_rowBound line 139
12. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.run_initial_size line 147
13. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.run_initial_product_le line 157