Results about big operators with values in an ordered algebraic structure. #
Mostly monotonicity results for the ∏
and ∑
operations.
Let {x | p x}
be an additive subsemigroup of an additive commutative monoid M
. Let
f : M → N
be a map subadditive on {x | p x}
, i.e., p x → p y → f (x + y) ≤ f x + f y
. Let
g i
, i ∈ s
, be a nonempty finite family of elements of M
such that ∀ i ∈ s, p (g i)
. Then
f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
.
Let {x | p x}
be a subsemigroup of a commutative monoid M
. Let f : M → N
be a map
submultiplicative on {x | p x}
, i.e., p x → p y → f (x * y) ≤ f x * f y
. Let g i
, i ∈ s
, be
a nonempty finite family of elements of M
such that ∀ i ∈ s, p (g i)
. Then
f (∏ x in s, g x) ≤ ∏ x in s, f (g x)
.
If f : M → N
is a submultiplicative function, f (x * y) ≤ f x * f y
and g i
, i ∈ s
, is a
nonempty finite family of elements of M
, then f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
.
If f : M → N
is a subadditive function, f (x + y) ≤ f x + f y
and g i
, i ∈ s
, is a
nonempty finite family of elements of M
, then f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
.
Let {x | p x}
be a subsemigroup of a commutative additive monoid M
. Let f : M → N
be a map
such that f 0 = 0
and f
is subadditive on {x | p x}
, i.e. p x → p y → f (x + y) ≤ f x + f y
.
Let g i
, i ∈ s
, be a finite family of elements of M
such that ∀ i ∈ s, p (g i)
. Then
f (∑ x in s, g x) ≤ ∑ x in s, f (g x)
.
Let {x | p x}
be a subsemigroup of a commutative monoid M
. Let f : M → N
be a map
such that f 1 = 1
and f
is submultiplicative on {x | p x}
, i.e.,
p x → p y → f (x * y) ≤ f x * f y
. Let g i
, i ∈ s
, be a finite family of elements of M
such
that ∀ i ∈ s, p (g i)
. Then f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
.
If f : M → N
is a submultiplicative function, f (x * y) ≤ f x * f y
, f 1 = 1
, and g i
,
i ∈ s
, is a finite family of elements of M
, then f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
.
If f : M → N
is a subadditive function, f (x + y) ≤ f x + f y
, f 0 = 0
, and g i
,
i ∈ s
, is a finite family of elements of M
, then f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
.
In an ordered additive commutative monoid, if each summand f i
of one finite sum is less than
or equal to the corresponding summand g i
of another finite sum, then
∑ i in s, f i ≤ ∑ i in s, g i
.
In an ordered commutative monoid, if each factor f i
of one finite product is less than or
equal to the corresponding factor g i
of another finite product, then
∏ i in s, f i ≤ ∏ i in s, g i
.
If every element belongs to at most n
finsets, then the sum of their sizes is at most n
times how many they are.
If every element belongs to at most n
finsets, then the sum of their sizes is at most n
times how many they are.
If every element belongs to at least n
finsets, then the sum of their sizes is at least n
times how many they are.
If every element belongs to at least n
finsets, then the sum of their sizes is at least n
times how many they are.
If every element belongs to exactly n
finsets, then the sum of their sizes is n
times how
many they are.
If every element belongs to exactly n
finsets, then the sum of their sizes is n
times how
many they are.
If all f i
, i ∈ s
, are nonnegative and each f i
is less than or equal to g i
, then the
product of f i
is less than or equal to the product of g i
. See also finset.prod_le_prod''
for
the case of an ordered commutative multiplicative monoid.
If each f i
, i ∈ s
belongs to [0, 1]
, then their product is less than or equal to one.
See also finset.prod_le_one'
for the case of an ordered commutative multiplicative monoid.
If g, h ≤ f
and g i + h i ≤ f i
, then the product of f
over s
is at least the
sum of the products of g
and h
. This is the version for ordered_comm_semiring
.
If g, h ≤ f
and g i + h i ≤ f i
, then the product of f
over s
is at least the
sum of the products of g
and h
. This is the version for canonically_ordered_comm_semiring
.
A product of finite numbers is still finite