OAI/Probability/InvariantIsing/Cavity/CavityLabeledSpin.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Labeled representation of the full cavity spin law and its field projection.

  1. def OAI.InvariantIsing.cavityLabeledSpinMap line 13
  2. lemma OAI.InvariantIsing.measurable_cavityLabeledSpinMap line 19
  3. lemma OAI.InvariantIsing.measurable_cavityLeafSpinPotential line 25
  4. theorem OAI.InvariantIsing.cavity_labeled_full_spin_law line 37
  5. theorem OAI.InvariantIsing.cavity_labeled_projected_spin_law line 73