OAI/Probability/InvariantIsing/Cavity/CavitySpectralStack.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The cavity column stack formed from square roots of spectral compressions. Its columns are orthonormal when the compressions sum to the identity, and it has the required deterministic limit.

  1. lemma OAI.InvariantIsing.cavity_sqrt_scalar_identity line 16
  2. def OAI.InvariantIsing.cavitySpectralStack line 22
  3. theorem OAI.InvariantIsing.cavitySpectralStack_gram line 26
  4. theorem OAI.InvariantIsing.cavitySpectralStack_tendsto line 46