English
Holley’s inequality: under certain monotonicity and normalization conditions, sums weighted by a measure preserve a certain majorization-type inequality between two nonnegative functions.
Русский
Неравенство Холли: при определённых монотонности и нормализации суммы, взвешенные меры сохраняют неравенство типа мажорирования между двумя неотрицательными функциями.
LaTeX
$$$$\\sum_{a} \\mu(a) f(a) \\le \\sum_{a} \\mu(a) g(a)$$ under suitable monotonicity and normalization hypotheses$$
Lean4
/-- Special case of the **Four Functions Theorem** when `s = t = univ`. -/
theorem four_functions_theorem_univ (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
(h : ∀ a b, f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)) : (∑ a, f₁ a) * ∑ a, f₂ a ≤ (∑ a, f₃ a) * ∑ a, f₄ a := by
classical simpa using four_functions_theorem f₁ f₂ f₃ f₄ h₁ h₂ h₃ h₄ h univ univ
