OAI/Probability/SKBarriers/Dynamics/BankNumerics.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.scheduledBankSize line 15
2. theorem OAI.SK.Analytic.scheduledBankSize_pos line 18
3. theorem OAI.SK.Analytic.eventually_exp_dominates_linear line 21
4. theorem OAI.SK.Analytic.greedy_level_count_bound line 30
5. theorem OAI.SK.Analytic.bank_miss_exp_bound line 39
6. theorem OAI.SK.Analytic.scheduled_bank_coverage_sum line 49
7. theorem OAI.SK.Analytic.scheduled_bank_locking_cost line 76