Solution (source code)

= Solution

Order configurations coordinatewise: $\omega\le\eta$ when $\omega(e)\le\eta(e)$ for every coordinate. An <increasing event> $A$ is an upward-closed set: $\omega\in A$ and $\omega\le\eta$ imply $\eta\in A$.

The finite-lattice <FKG inequality> states that a <probability> mass function satisfying the <FKG lattice condition>
$$
\mu(\omega\vee\eta)\mu(\omega\wedge\eta)\ge\mu(\omega)\mu(\eta)
\quad\text{for every }\omega,\eta
$$
is <positively associated>. Here <meet in a lattice> and <join in a lattice> are coordinatewise minimum and maximum. Thus for <increasing observables> $f,g$,
$$
E_\mu[fg]\ge E_\mu[f]E_\mu[g].
$$
Taking <indicator functions> gives \b[$\mu(A\cap B)\ge\mu(A)\mu(B)$ for all <increasing events>]. The strictly positive version suffices for the Ising weights here; the theorem also holds for nonnegative log-supermodular weights of positive total mass.