OAI/Probability/InvariantIsing/Cavity/CavityProjectedRestrictedNumerator.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The hard-restricted marked spin moment is the actual Gibbs numerator with the same restriction on every replica.

  1. lemma OAI.InvariantIsing.cavity_projected_restricted_spin_numerator line 15