OAI/Probability/InvariantIsing/Magnetic/MagneticWassersteinPressure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Theorem7.1 for general W1 field laws, with mean and almost-sure convergence.

  1. theorem OAI.InvariantIsing.limiting_wasserstein_field_pressure line 12