OAI/Probability/InvariantIsing/Cavity/CavityHaarRestrictedSpinMatch.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The hard-restricted physical Haar spin moments match the strict finite Gaussian cavity moments. The cutoff is taken at a common continuity radius of the limiting marked law.

  1. theorem OAI.InvariantIsing.cavity_haar_strict_restricted_spin_match line 16