English
Fortuin–Kasteleyn–Ginibre inequality: for certain positively correlated random-like functions, the expectation of the product is at most the product of expectations when the functions are monotone with respect to a lattice structure.
Русский
Неравенство Фог-Кастейлина-Гинибра: при условиях положительной корреляции неотрицательных функций и монотонности по решётке, ожидание произведения не превосходит произведение ожиданий.
LaTeX
$$$$\\left(\\sum_{a} \\mu(a) f(a)\\right)\\left(\\sum_{a} \\mu(a) g(a)\\right) \\le \\left(\\sum_{a} \\mu(a)\\right)\\left(\\sum_{a} \\mu(a) (f(a) g(a))\\right)$$$$
Lean4
/-- The **Holley Inequality**. -/
theorem holley (hμ₀ : 0 ≤ μ) (hf : 0 ≤ f) (hg : 0 ≤ g) (hμ : Monotone μ) (hfg : ∑ a, f a = ∑ a, g a)
(h : ∀ a b, f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)) : ∑ a, μ a * f a ≤ ∑ a, μ a * g a := by
classical
obtain rfl | hf := hf.eq_or_lt
· simp only [Pi.zero_apply, sum_const_zero, eq_comm, Fintype.sum_eq_zero_iff_of_nonneg hg] at hfg
simp [hfg]
obtain rfl | hg := hg.eq_or_lt
· simp only [Pi.zero_apply, sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg
simp [hfg]
have :=
four_functions_theorem g (μ * f) f (μ * g) hg.le (mul_nonneg hμ₀ hf.le) hf.le (mul_nonneg hμ₀ hg.le) (fun a b ↦ ?_)
univ univ
· simpa [hfg, sum_pos hg] using this
· simp_rw [Pi.mul_apply, mul_left_comm _ (μ _), mul_comm (g _)]
rw [sup_comm, inf_comm]
exact mul_le_mul (hμ le_sup_left) (h _ _) (mul_nonneg (hf.le _) <| hg.le _) <| hμ₀ _
