OAI/Probability/InvariantIsing/Magnetic/MagneticRationalBlockLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual rational-spectrum block laws supply the diagonal magnetic trial lower bound.

  1. theorem OAI.InvariantIsing.magnetic_rational_block_diagonal_lower line 12