OAI/Probability/InvariantIsing/Cavity/CavityHaarCutoffComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The original Ising cutoff, averaged over its actual Haar disorder, is compared with an independent Haar base cavity law. All random block coefficients remain inside the normalized test.

  1. theorem OAI.InvariantIsing.cavity_haar_cutoff_comparison line 18