OAI/Probability/InvariantIsing/Magnetic/MagneticMainPressure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-field clause of Theorem7.1 with the exact manuscript spectral-edge assumptions, in expectation and almost surely.

  1. theorem OAI.InvariantIsing.limiting_finite_field_pressure_of_extreme_limits line 13