OAI/Probability/InvariantIsing/Spectral/SpectralApproximationSqueeze.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The final two-scale squeeze used in compact spectral approximation.
- lemma
OAI.InvariantIsing.spectral_approximation_squeezeline 14