Big operators #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define products and sums indexed by finite sets (specifically, finset
).
Notation #
We introduce the following notation, localized in big_operators
.
To enable the notation, use open_locale big_operators
.
Let s
be a finset α
, and f : α → β
a function.
∏ x in s, f x
is notation forfinset.prod s f
(assumingβ
is acomm_monoid
)∑ x in s, f x
is notation forfinset.sum s f
(assumingβ
is anadd_comm_monoid
)∏ x, f x
is notation forfinset.prod finset.univ f
(assumingα
is afintype
andβ
is acomm_monoid
)∑ x, f x
is notation forfinset.sum finset.univ f
(assumingα
is afintype
andβ
is anadd_comm_monoid
)
Implementation Notes #
The first arguments in all definitions and lemmas is the codomain of the function of the big
operator. This is necessary for the heuristic in @[to_additive]
.
See the documentation of to_additive.attr
for more information.
∑ x in s, f x
is the sum of f x
as x
ranges over the elements
of the finite set s
.
Equations
- s.sum f = (multiset.map f s.val).sum
∏ x in s, f x
is the product of f x
as x
ranges over the elements of the finite set s
.
Equations
- s.prod f = (multiset.map f s.val).prod
There is no established mathematical convention
for the operator precedence of big operators like ∏
and ∑
.
We will have to make a choice.
Online discussions, such as https://math.stackexchange.com/q/185538/30839
seem to suggest that ∏
and ∑
should have the same precedence,
and that this should be somewhere between *
and +
.
The latter have precedence levels 70
and 65
respectively,
and we therefore choose the level 67
.
In practice, this means that parentheses should be placed as follows:
∑ k in K, (a k + b k) = ∑ k in K, a k + ∑ k in K, b k →
∏ k in K, a k * b k = (∏ k in K, a k) * (∏ k in K, b k)
(Example taken from page 490 of Knuth's Concrete Mathematics.)
Deprecated: use _root_.map_sum
instead.
Deprecated: use _root_.map_prod
instead.
Deprecated: use _root_.map_sum
instead.
Deprecated: use _root_.map_prod
instead.
Deprecated: use _root_.map_list_sum
instead.
A morphism into the opposite ring acts on the product by acting on the reversed elements.
Deprecated: use _root_.unop_map_list_prod
instead.
Deprecated: use _root_.map_multiset_prod
instead.
Deprecated: use _root_.map_multiset_sum
instead.
Deprecated: use _root_.map_prod
instead.
Deprecated: use _root_.map_sum
instead.
The sum of f
over insert a s
is the same as
the sum over s
, as long as a
is in s
or f a = 0
.
The product of f
over insert a s
is the same as
the product over s
, as long as a
is in s
or f a = 1
.
The sum of f
over insert a s
is the same as
the sum over s
, as long as f a = 0
.
The product of f
over insert a s
is the same as the product over s
, as long as f a = 1
.
Adding the sums of a function over s
and over sᶜ
gives the whole sum.
For a version expressed with subtypes, see fintype.sum_subtype_add_sum_subtype
.
Multiplying the products of a function over s
and over sᶜ
gives the whole product.
For a version expressed with subtypes, see fintype.prod_subtype_mul_prod_subtype
.
Reorder a sum.
The difference with sum_bij'
is that the bijection is specified as a surjective injection,
rather than by an inverse function.
Reorder a product.
The difference with prod_bij'
is that the bijection is specified as a surjective injection,
rather than by an inverse function.
Reorder a sum.
The difference with sum_bij
is that the bijection is specified with an inverse, rather than
as a surjective injection.
Reorder a product.
The difference with prod_bij
is that the bijection is specified with an inverse, rather than
as a surjective injection.
Reindexing a product over a finset along an equivalence.
See equiv.prod_comp
for the version where s
and s'
are univ
.
Reindexing a sum over a finset along an equivalence.
See equiv.sum_comp
for the version where s
and s'
are univ
.
Generalization of finset.sum_comm
to the case when the inner finset
s depend on
the outer variable.
Generalization of finset.prod_comm
to the case when the inner finset
s depend on the outer
variable.
A product over s.subtype p
equals one over s.filter p
.
A sum over s.subtype p
equals one over s.filter p
.
If all elements of a finset
satisfy the predicate p
, a product
over s.subtype p
equals that product over s
.
If all elements of a finset
satisfy the predicate p
, a sum
over s.subtype p
equals that sum over s
.
A sum of a function over a finset
in a subtype equals a
sum in the main type of a function that agrees with the first
function on that finset
.
A product of a function over a finset
in a subtype equals a
product in the main type of a function that agrees with the first
function on that finset
.
The sum of a function g
defined only on a set s
is equal to
the sum of a function f
defined everywhere,
as long as f
and g
agree on s
, and f = 0
off s
.
The product of a function g
defined only on a set s
is equal to
the product of a function f
defined everywhere,
as long as f
and g
agree on s
, and f = 1
off s
.
A sum taken over a conditional whose condition is an equality test on the index
and whose alternative is 0
has value either the term at that index or 0
.
The difference with finset.sum_ite_eq
is that the arguments to eq
are swapped.
A product taken over a conditional whose condition is an equality test on the index and whose
alternative is 1
has value either the term at that index or 1
.
The difference with finset.prod_ite_eq
is that the arguments to eq
are swapped.
To prove a property of a product, it suffices to prove that the property is multiplicative and holds on factors.
To prove a property of a sum, it suffices to prove that the property is additive and holds on summands.
To prove a property of a sum, it suffices to prove that the property is additive and holds on summands.
To prove a property of a product, it suffices to prove that the property is multiplicative and holds on factors.
For any product along {0, ..., n - 1}
of a commutative-monoid-valued function, we can verify
that it's equal to a different function just by checking ratios of adjacent terms.
This is a multiplicative discrete analogue of the fundamental theorem of calculus.
For any sum along {0, ..., n - 1}
of a commutative-monoid-valued function, we can
verify that it's equal to a different function just by checking differences of adjacent terms.
This is a discrete analogue of the fundamental theorem of calculus.
A telescoping sum along {0, ..., n - 1}
of an additive commutative group valued
function reduces to the difference of the last and first terms.
A telescoping product along {0, ..., n - 1}
of a commutative group valued function reduces to
the ratio of the last and first factors.
A telescoping sum along {0, ..., n-1}
of an ℕ
-valued function
reduces to the difference of the last and first terms
when the function we are summing is monotone.
The product of the composition of functions f
and g
, is the product over b ∈ s.image g
of
f b
to the power of the cardinality of the fibre of b
. See also finset.prod_image
.
The sum of the composition of functions f
and g
, is the sum over b ∈ s.image g
of f b
times of the cardinality of the fibre of b
. See also finset.sum_image
.