OAI/Probability/InvariantIsing/Fields/SpinFiniteCoverMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Haar fluctuations allow a fixed finite spin cover to be used inside the expectation of the full pressure.

  1. theorem OAI.InvariantIsing.haar_finite_cover_mean_pressure_upper line 13