OAI/Probability/InvariantIsing/Magnetic/MagneticAdjacentSquare.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The conditional square means preceding a transferred variance increment decrease at fixed total mean spin.

  1. theorem OAI.InvariantIsing.magneticClosedSquare_adjacent_transfer line 14