English
Let A be a totally ordered commutative monoid and s a multiset of indices. For any functions f, g : ι → A, the larger of the two products ∏_{i∈s} f(i) and ∏_{i∈s} g(i) is bounded above by the product over s of the pointwise maxima max(f(i), g(i)).
Русский
Пусть A — упорядоченная коммойн-моноида, и пусть s — мультимножество индексов. Для любых функций f, g : ι → A верно, что максимум из произведений по s значений f и g не превосходит произведение по s максимумов по каждой координате: ∏_{i∈s} max(f(i), g(i)).
LaTeX
$$$$\\max\\left(\\prod_{i \\in s} f(i),\\ \\prod_{i \\in s} g(i)\\right) \\le \\prod_{i \\in s} \\max\\bigl(f(i),\\, g(i)\\bigr).$$$$
Lean4
@[to_additive]
theorem max_prod_le [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] {s : Multiset ι} {f g : ι → α} :
max (s.map f).prod (s.map g).prod ≤ (s.map fun i ↦ max (f i) (g i)).prod :=
by
obtain ⟨l⟩ := s
simp_rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
apply List.max_prod_le
