OAI/Probability/SKBarriers/Replicas/ReplicaSampling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.FiniteLaw.iid_expect_involutions line 17
2. theorem OAI.SK.Analytic.FiniteLaw.iid_two_then_one line 29
3. def OAI.SK.Analytic.orient line 50
4. theorem OAI.SK.Analytic.orient_orient line 52
5. theorem OAI.SK.Analytic.gibbs_orient line 54
6. theorem OAI.SK.Analytic.overlap_orient_abs line 56
7. theorem OAI.SK.Analytic.iid_gibbs_replica line 63
8. theorem OAI.SK.Analytic.iid_gibbs_oriented_replica line 69
9. theorem OAI.SK.Analytic.bank_triple_oriented line 77
10. theorem OAI.SK.Analytic.bank_pair_vertex_oriented line 94