OAI/Probability/InvariantIsing/Magnetic/RestrictedPhysicalLogSplit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal constrained log-partition increment, including the cavity slice's original cube mass, is its Gibbs cavity logarithm.

  1. theorem OAI.InvariantIsing.restricted_cavity_spin_leaf_log_increment line 14