OAI/Probability/InvariantIsing/Spectral/SpectralArrayEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The interaction before temperature multiplication is an exact bounded continuous spectral-array observable, so its Gibbs mean passes to weak limits.

  1. lemma OAI.InvariantIsing.normalized_rotatedEnergy_eq_blocks line 16
  2. def OAI.InvariantIsing.spectralArrayInteractionEnergy line 40
  3. lemma OAI.InvariantIsing.continuous_spectralArrayInteractionEnergy line 44
  4. lemma OAI.InvariantIsing.tensorNamespacedArrayLaw_interactionEnergy line 49
  5. lemma OAI.InvariantIsing.spectralArrayInteractionEnergy_weak_limit line 70
  6. lemma OAI.InvariantIsing.spectralArrayInteractionEnergy_eq_finiteEnergy line 80