Big operators on a multiset in ordered groups with zeros #
This file contains the results concerning the interaction of multiset big operators with ordered groups with zeros.
theorem
Multiset.prod_nonneg
{R : Type u_1}
[CommMonoidWithZero R]
[PartialOrder R]
[ZeroLEOneClass R]
[PosMulMono R]
{s : Multiset R}
(h : ∀ a ∈ s, 0 ≤ a)
:
0 ≤ s.prod
theorem
Multiset.one_le_prod
{R : Type u_1}
[CommMonoidWithZero R]
[PartialOrder R]
[ZeroLEOneClass R]
[PosMulMono R]
{s : Multiset R}
(h : ∀ a ∈ s, 1 ≤ a)
:
1 ≤ s.prod
theorem
Multiset.prod_map_le_prod_map₀
{R : Type u_1}
[CommMonoidWithZero R]
[PartialOrder R]
[ZeroLEOneClass R]
[PosMulMono R]
{ι : Type u_2}
{s : Multiset ι}
(f : ι → R)
(g : ι → R)
(h0 : ∀ i ∈ s, 0 ≤ f i)
(h : ∀ i ∈ s, f i ≤ g i)
:
(Multiset.map f s).prod ≤ (Multiset.map g s).prod
theorem
Multiset.prod_pos
{R : Type u_1}
[CommMonoidWithZero R]
[PartialOrder R]
[ZeroLEOneClass R]
[PosMulStrictMono R]
[NeZero 1]
{s : Multiset R}
(h : ∀ a ∈ s, 0 < a)
:
0 < s.prod
theorem
Multiset.prod_map_lt_prod_map
{R : Type u_1}
[CommMonoidWithZero R]
[PartialOrder R]
[ZeroLEOneClass R]
[PosMulStrictMono R]
[NeZero 1]
{ι : Type u_2}
{s : Multiset ι}
(hs : s ≠ 0)
(f : ι → R)
(g : ι → R)
(h0 : ∀ i ∈ s, 0 < f i)
(h : ∀ i ∈ s, f i < g i)
:
(Multiset.map f s).prod < (Multiset.map g s).prod