OAI/Probability/InvariantIsing/Cavity/ConsecutiveProductTreeSpin.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The averaged last-block spin insertion is the full weighted-overlap observable, including the original random cascade tree.

  1. theorem OAI.InvariantIsing.consecutive_product_tree_spin_identity line 14