OAI/Probability/InvariantIsing/Cavity/CavitySpinPrior.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact prior symmetries for the signed-site action. The cascade leaf coordinate stays fixed and retains its original random prior.

  1. lemma OAI.InvariantIsing.uniformSpinPrior_equiv line 14
  2. lemma OAI.InvariantIsing.labeledSpinReference_equiv line 30