OAI/Probability/InvariantIsing/Magnetic/MagneticLimitingPressure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-alphabet part of manuscript Theorem7.1, with arbitrary compact spectrum, expectation convergence and almost-sure convergence.

  1. theorem OAI.InvariantIsing.limiting_finite_field_pressure line 13