OAI/Probability/SKBarriers/Dynamics/BankAvoidance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.iid_gibbs_oriented_permuted_replica line 14
2. theorem OAI.SK.Analytic.bank_pair_vertex_permuted line 22
3. theorem OAI.SK.Analytic.FiniteLaw.expect_prob_exists_le line 35
4. def OAI.SK.Analytic.bankTripleBad line 41
5. def OAI.SK.Analytic.bankVertexBad line 47
6. theorem OAI.SK.Analytic.bankTripleBad_prob line 53
7. theorem OAI.SK.Analytic.expected_bankVertexBad line 72
8. theorem OAI.SK.Analytic.exists_fixed_good_bank line 89