OAI/Probability/InvariantIsing/Spectral/SpectralDiagonalWardLimits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Weak closure of the one-replica diagonal Ward residual.

  1. def OAI.InvariantIsing.spectralDiagonalWardResidual line 14
  2. lemma OAI.InvariantIsing.spectralDiagonalWardResidual_constant_diagonal line 21
  3. lemma OAI.InvariantIsing.spectralDiagonalWardResidual_weak_limit line 53
  4. theorem OAI.InvariantIsing.spectralDiagonalWardResidual_zero_of_vanishing_bound line 73