OAI/Probability/InvariantIsing/Cavity/CavityHaarFiniteCutoff.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual Haar restricted Gibbs test approaches the full finite spectral cavity test as the cutoff grows after the system-size limit.

  1. theorem OAI.InvariantIsing.cavity_haar_finite_cutoff_comparison line 18