OAI/Combinatorics/MatchingCount/Complexity/OnlineHistoryCost.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.all_of_qaverage line 7
2. def OAI.MatchingFPRAS.OnlineTrial.initial line 23
3. def OAI.MatchingFPRAS.OnlineTrial.History line 25
4. lemma OAI.MatchingFPRAS.OnlineTrial.history_initial line 28
5. lemma OAI.MatchingFPRAS.OnlineTrial.history_size line 30
6. lemma OAI.MatchingFPRAS.OnlineTrial.history_step line 34
7. lemma OAI.MatchingFPRAS.OnlineTrial.sweep_history line 46
8. lemma OAI.MatchingFPRAS.OnlineTrial.sweep_bound line 61