OAI/Probability/InvariantIsing/Cavity/CavityGoodCompression.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous control of the finitely many spectral compression blocks, obtained from their positive limiting proportions.

  1. theorem OAI.InvariantIsing.cavityHaarWindow_correction_all line 14