OAI/Probability/InvariantIsing/Cavity/CavityHaarCutoffLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

At a fixed spatial cutoff the original spin test converges to the independent base-Haar cavity test with deterministic limiting blocks.

  1. theorem OAI.InvariantIsing.cavity_haar_cutoff_limit line 16