OAI/Probability/InvariantIsing/Cavity/CavityCanonicalBlockLimit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Canonical spectral-group blocks of finite cascades converge to the actual Ward-identified spectral array. The auxiliary tree coordinate is not needed by these physical group observables.

  1. def OAI.InvariantIsing.cavityCanonicalDiagonal line 16
  2. def OAI.InvariantIsing.cavitySpectralGroupBlock line 22
  3. lemma OAI.InvariantIsing.continuous_cavitySpectralGroupBlock line 25
  4. lemma OAI.InvariantIsing.cavity_spectral_spin_gram line 30
  5. theorem OAI.InvariantIsing.cavity_canonical_group_block_tendsto line 43