OAI/Probability/InvariantIsing/Magnetic/RestrictedHaarSymmetry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full finite Ising model with its actual spectral/tree tensor perturbation has signed site-permutation symmetry after Haar averaging.

  1. theorem OAI.InvariantIsing.restricted_full_signed_site_symmetry line 15