OAI/Probability/InvariantIsing/Magnetic/MagneticPairComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A dimension-free comparison of the actual constrained two-spin mean with the site-average magnetic field law.

  1. def OAI.InvariantIsing.restrictedBlockPairMean line 15
  2. theorem OAI.InvariantIsing.restrictedBlockPairMean_comparison line 20