prod_map_le_pow_length₀ — Mathlib

English

If 0 ≤ f(x) ≤ r for all x in t, then the product of f over t is at most r raised to the length of t: (∏ f(x)) ≤ r^{|t|}.

Русский

Если для всех x∈t выполняется 0 ≤ f(x) ≤ r, то произведение по t не превосходит r^{|t|}.

LaTeX

$$$$\\prod_{x \\in t} f(x) \\le r^{|t|} \\quad \\text{given } 0 \\le f(x) \\le r \\text{ for all } x \\in t.$$$$

Lean4

theorem prod_map_le_pow_length₀ {F L : Type*} [FunLike F L R] {f : F} {r : R} {t : List L} (hf0 : ∀ x ∈ t, 0 ≤ f x)
    (hf : ∀ x ∈ t, f x ≤ r) : (map f t).prod ≤ r ^ length t :=
  by
  convert prod_map_le_prod_map₀ f (Function.const L r) hf0 hf
  simp [map_const, prod_replicate]

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