OAI/Probability/InvariantIsing/Cavity/CavitySpinProduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Product-prior factorization of the capped cavity replica test. This connects the physical base-spin/cavity-spin replicas to the Haar test.

  1. theorem OAI.InvariantIsing.cavity_capped_spin_product line 14