OAI/Probability/FreeIsing/Trees/ColoredPathEndpoints.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem367.prefixFlip_reduced_consline 8 - theorem
OAI.Problem367.prefixFlip_reduced_dropLastline 17 - def
OAI.Problem367.ColoredPathAverage.tailVertexline 33 - def
OAI.Problem367.ColoredPathAverage.headVertexline 36 - theorem
OAI.Problem367.ColoredPathAverage.headVertex_succline 39 - theorem
OAI.Problem367.ColoredPathAverage.tailVertex_succline 44 - theorem
OAI.Problem367.ColoredPathAverage.pathValue_eq_edgeVectorline 55