OAI/Probability/SKBarriers/Replicas/ReplicaCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.tripleR line 14
2. def OAI.SK.Analytic.tripleDelta line 15
3. def OAI.SK.Analytic.tripleQ line 16
4. theorem OAI.SK.Analytic.replicaGram_pair_overlap line 18
5. theorem OAI.SK.Analytic.replicaGram_triple_overlap line 24
6. theorem OAI.SK.Analytic.replicaGram_feasible line 29
7. theorem OAI.SK.Analytic.tripleQ_flip line 33
8. theorem OAI.SK.Analytic.tripleR_flip line 36
9. theorem OAI.SK.Analytic.tripleDelta_flip line 45
10. theorem OAI.SK.Analytic.tripleRDelta_abs_le line 54