OAI/Probability/SKBarriers/Dynamics/BankCoverage.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.FiniteLaw.iid_random_cell_miss line 16
2. abbrev OAI.SK.Analytic.BankIndex line 36
3. abbrev OAI.SK.Analytic.BankPrior line 37
4. abbrev OAI.SK.Analytic.BankTuple line 38
5. def OAI.SK.Analytic.bankJointIndex line 41
6. theorem OAI.SK.Analytic.bankJointIndex_injective line 45
7. def OAI.SK.Analytic.bankCell line 67
8. def OAI.SK.Analytic.bankCoverageBad line 71
9. theorem OAI.SK.Analytic.expected_bank_coverage_bad line 76