OAI/Probability/SKBarriers/Dynamics/BankCardinality.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.bankPrefix line 13
2. theorem OAI.SK.Analytic.bankPrefix_nonneg line 17
3. theorem OAI.SK.Analytic.bankPrefix_mono line 22
4. theorem OAI.SK.Analytic.bankPrefix_cost_le line 28
5. def OAI.SK.Analytic.blockPriorEquiv line 33
6. theorem OAI.SK.Analytic.blockPriorEquiv_mod line 57
7. theorem OAI.SK.Analytic.bankPrefix_sum line 63
8. theorem OAI.SK.Analytic.bankTuple_card_bound line 68
9. theorem OAI.SK.Analytic.bankIndex_card_bound line 91
10. theorem OAI.SK.Analytic.ceil_exp_bound line 104