English
If a multiplicative function f on a monoid is nonnegative and submultiplicative, then for any finite set of arguments g with a predicate p preserved, f(∏ g_i) ≤ ∏ f(g_i).
Русский
Если f на моноиде неотрицательна и подумножается, то для любых аргументов g на конечном множестве выполняется неравенство: f(∏ g_i) ≤ ∏ f(g_i).
LaTeX
$$$$f\\Bigl(\\prod_{i \\in s} g(i)\\Bigr) \\le \\prod_{i \\in s} f(g(i)).$$$$
Lean4
/-- If `g, h ≤ f` and `g i + h i ≤ f i`, then the product of `f` over `s` is at least the
sum of the products of `g` and `h`. This is the version for `OrderedCommSemiring`. -/
theorem prod_add_prod_le {i : ι} {f g h : ι → R} (hi : i ∈ s) (h2i : g i + h i ≤ f i) (hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j)
(hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j) (hg : ∀ i ∈ s, 0 ≤ g i) (hh : ∀ i ∈ s, 0 ≤ h i) :
((∏ i ∈ s, g i) + ∏ i ∈ s, h i) ≤ ∏ i ∈ s, f i := by
classical
simp_rw [prod_eq_mul_prod_diff_singleton hi]
refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
· rw [right_distrib]
gcongr with j hj <;> aesop
· apply prod_nonneg
simp only [and_imp, mem_sdiff, mem_singleton]
exact fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)
