English
Fortuin–Kasteleyn–Ginibre inequality, same as above in another formulation for monotone families.
Русский
Неравенство Фог-Кастейлина-Гинибре, другое формулирование для монотонных семейств.
LaTeX
$$$$\\text{FKG: } \\mathbb{E}[FG]\\le \\mathbb{E}[F]\\mathbb{E}[G] \\text{ for monotone } F,G$$$$
Lean4
/-- The **Fortuin-Kastelyn-Ginibre Inequality**. -/
theorem fkg (hμ₀ : 0 ≤ μ) (hf₀ : 0 ≤ f) (hg₀ : 0 ≤ g) (hf : Monotone f) (hg : Monotone g)
(hμ : ∀ a b, μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)) :
(∑ a, μ a * f a) * ∑ a, μ a * g a ≤ (∑ a, μ a) * ∑ a, μ a * (f a * g a) :=
by
refine
four_functions_theorem_univ (μ * f) (μ * g) μ _ (mul_nonneg hμ₀ hf₀) (mul_nonneg hμ₀ hg₀) hμ₀
(mul_nonneg hμ₀ <| mul_nonneg hf₀ hg₀) (fun a b ↦ ?_)
dsimp
rw [mul_mul_mul_comm, ← mul_assoc (μ (a ⊓ b))]
exact
mul_le_mul (hμ _ _) (mul_le_mul (hf le_sup_left) (hg le_sup_right) (hg₀ _) <| hf₀ _)
(mul_nonneg (hf₀ _) <| hg₀ _) <|
mul_nonneg (hμ₀ _) <| hμ₀ _
