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)
:
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)
:
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 g : ι → R)
(h0 : ∀ i ∈ s, 0 ≤ f i)
(h : ∀ i ∈ s, f i ≤ g i)
:
theorem
Multiset.prod_map_le_pow_card
{R : Type u_1}
[CommMonoidWithZero R]
[PartialOrder R]
[ZeroLEOneClass R]
[PosMulMono R]
{F : Type u_2}
{L : Type u_3}
[FunLike F L R]
{f : F}
{r : R}
{t : Multiset L}
(hf0 : ∀ x ∈ t, 0 ≤ f x)
(hf : ∀ x ∈ t, f x ≤ r)
:
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)
:
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 g : ι → R)
(h0 : ∀ i ∈ s, 0 < f i)
(h : ∀ i ∈ s, f i < g i)
: