OAI/Probability/InvariantIsing/Fields/PriorEnergyLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The original interaction energy in a constrained-prior GG limit is identified by the actual rotation Ward equations.

  1. lemma OAI.InvariantIsing.priorNamespacedObservableAverage_eq_replica_one line 16
  2. lemma OAI.InvariantIsing.priorNamespacedArrayLaw_interactionEnergy line 31
  3. theorem OAI.InvariantIsing.priorPerturbedArrayLaw_interactionEnergy_limit line 51