le_prod_of_submultiplicative_of_nonneg

English

A variant for nonnegative functions on finite sets: f(∏ g_i) ≤ ∏ f(g_i) under nonnegativity and submultiplicativity assumptions.

Русский

Вариант для неотрицательных функций на конечном множестве: неравенство сохраняется.

LaTeX

$$$$f\\left(\\prod_{i \\in s} g(i)\\right) \\le \\prod_{i \\in s} f(g(i)).$$$$

Lean4

theorem le_prod_of_submultiplicative_of_nonneg {M : Type*} [CommMonoid M] (f : M → R) (h_nonneg : ∀ a, 0 ≤ f a)
    (h_one : f 1 ≤ 1) (h_mul : ∀ x y : M, f (x * y) ≤ f x * f y) (s : Finset ι) (g : ι → M) :
    f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) :=
  le_trans (Multiset.le_prod_of_submultiplicative_of_nonneg f h_nonneg h_one h_mul _) (by simp [Multiset.map_map])

Похожие утверждения