Negative correlation of antitone and monotone functions

[UPSTREAM] The Fortuin–Kasteleyn–Ginibre inequality (fkg) says that under a log-supermodular weight two monotone functions are positively correlated. Replacing one of them by its reflection gives the negative form: an antitone and a monotone function are negatively correlated, so reweighting by an antitone factor lowers the mass of every upper set.

theorem fkg_antitone_monotone {α : Type u_1} {β : Type u_2} [DistribLattice α] [Fintype α] [CommRing β] [LinearOrder β] [IsStrictOrderedRing β] {μ f g : α → β} (hμ₀ : 0 ≤ μ) (hf₀ : 0 ≤ f) (hg₀ : 0 ≤ g) (hf : Antitone f) (hg : Monotone g) (hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)) : (∑ a : α, μ a) * ∑ a : α, μ a * (f a * g a) ≤ (∑ a : α, μ a * f a) * ∑ a : α, μ a * g a

Under a log-supermodular weight, an antitone and a monotone function are negatively correlated.