OAI/Probability/InvariantIsing/Spectral/SpectralProjectionMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Haar-averaged squared projections are constant within each eigenspace. This follows from the finite coordinate Ward identity and holds for any fixed nonzero nonnegative spin prior, including deterministic fields.

  1. def OAI.InvariantIsing.meanCoordinateSquare line 16
  2. lemma OAI.InvariantIsing.integrable_gibbsCoordinateSquare line 21
  3. lemma OAI.InvariantIsing.meanCoordinateSquare_nonneg line 35
  4. lemma OAI.InvariantIsing.sum_meanCoordinateSquare line 44
  5. lemma OAI.InvariantIsing.meanCoordinateSquare_eq_of_eigenvalue_eq line 62