OAI/Combinatorics/MatchingCount/Algorithm/GuardBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingFPRAS.FiniteTrial.oneBits_le_trial line 10
2. lemma OAI.MatchingFPRAS.FiniteTrial.guardedBits_le line 17
3. lemma OAI.MatchingFPRAS.FiniteTrial.guardedAmplifiedBits_le line 21
4. theorem OAI.MatchingFPRAS.BitComplexity.polynomial_guarded_bits line 30
5. lemma OAI.MatchingFPRAS.FiniteTrial.padded_guarded_success line 44
6. theorem OAI.MatchingFPRAS.FiniteTrial.guarded_scheduled_fair_tapes line 52