OAI/Probability/InvariantIsing/Fields/SpinPriorEnergyLimit.lean

GitHub source file

4 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.spinPriorPerturbedArrayLaw_partition line 18
  2. lemma OAI.InvariantIsing.spinPriorObservableAverage_eq_replica_one line 31
  3. lemma OAI.InvariantIsing.spinPriorArrayLaw_interactionEnergy line 46
  4. theorem OAI.InvariantIsing.spinPriorPerturbedArrayLaw_interactionEnergy_limit line 66