OAI/Probability/InvariantIsing/Magnetic/RestrictedSpinSymmetry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A spin permutation preserving a constraint preserves its normalized prior and its product with the actual cascade leaf law.

  1. theorem OAI.InvariantIsing.restrictedSpinPrior_equiv line 14
  2. theorem OAI.InvariantIsing.restricted_labeled_spin_reference_equiv line 34