OAI/Probability/InvariantIsing/Fields/PriorLabeledRootPair.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Common-depth spin tests of the actual rooted kernel in labeled coordinates.

  1. theorem OAI.InvariantIsing.prior_cavity_labeled_rooted_spin_pair line 15