OAI/Probability/InvariantIsing/Magnetic/RestrictedSpinLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The constrained terminal spin distribution is the physical Gibbs law conditioned on the allowed spins. Its entropy cost is exactly the loss in log partition functions, retaining the original cube mass.

  1. lemma OAI.InvariantIsing.spinGibbs_mass_finset line 17
  2. lemma OAI.InvariantIsing.spinGibbs_mass_pos line 27
  3. def OAI.InvariantIsing.restrictedSpinLaw line 32
  4. lemma OAI.InvariantIsing.restrictedSpinLaw_probability line 35
  5. theorem OAI.InvariantIsing.restrictedSpinLaw_entropy line 40