Infinite sum and product over a topological monoid #
This file defines unconditionally convergent sums over a commutative topological additive monoid. For Euclidean spaces (finite dimensional Banach spaces) this is equivalent to absolute convergence.
We also define unconditionally convergent products over a commutative topological multiplicative monoid.
Note: There are summable sequences which are not unconditionally convergent! The other way holds
generally, see HasSum.tendsto_sum_nat
.
Implementation notes #
We say that a function f : β → α
has an unconditional product of a
if the function
fun s : Finset β ↦ ∏ b ∈ s, f b
converges to a
on the atTop
filter on Finset β
. In other
words, for every neighborhood U
of a
, there exists a finite set s : Finset β
of indices such
that ∏ b ∈ s', f b ∈ U
for any finite set s'
which is a superset of s
.
This may yield some unexpected results. For example, according to this definition, the product
∏' n : ℕ, (1 : ℝ) / 2
unconditionally exists and is equal to 0
. More strikingly,
the product ∏' n : ℕ, (n : ℝ)
unconditionally exists and is equal to 0
, because one
of its terms is 0
(even though the product of the remaining terms diverges). Users who would
prefer that these products be considered not to exist can carry them out in the unit group ℝˣ
rather than in ℝ
.
References #
- Bourbaki: General Topology (1995), Chapter 3 §5 (Infinite sums in commutative groups)
HasProd f a
means that the (potentially infinite) product of the f b
for b : β
converges
to a
.
The atTop
filter on Finset β
is the limit of all finite sets towards the entire type. So we take
the product over bigger and bigger sets. This product operation is invariant under reordering.
For the definition and many statements, α
does not need to be a topological monoid. We only add
this assumption later, for the lemmas where it is relevant.
These are defined in an identical way to infinite sums (HasSum
). For example, we say that
the function ℕ → ℝ
sending n
to 1 / 2
has a product of 0
, rather than saying that it does
not converge as some authors would.
Equations
- HasProd f a = Filter.Tendsto (fun (s : Finset β) => ∏ b ∈ s, f b) Filter.atTop (nhds a)
Instances For
HasSum f a
means that the (potentially infinite) sum of the f b
for b : β
converges to a
.
The atTop
filter on Finset β
is the limit of all finite sets towards the entire type. So we sum
up bigger and bigger sets. This sum operation is invariant under reordering. In particular,
the function ℕ → ℝ
sending n
to (-1)^n / (n+1)
does not have a
sum for this definition, but a series which is absolutely convergent will have the correct sum.
This is based on Mario Carneiro's
infinite sum df-tsms
in Metamath.
For the definition and many statements, α
does not need to be a topological monoid. We only add
this assumption later, for the lemmas where it is relevant.
Equations
- HasSum f a = Filter.Tendsto (fun (s : Finset β) => ∑ b ∈ s, f b) Filter.atTop (nhds a)
Instances For
Multipliable f
means that f
has some (infinite) product. Use tprod
to get the value.
Equations
- Multipliable f = ∃ (a : α), HasProd f a
Instances For
∏' i, f i
is the product of f
if it exists and is unconditionally convergent,
or 1 otherwise.
Equations
- tprod f = if h : Multipliable f then if (Function.mulSupport f).Finite then finprod f else Exists.choose h else 1
Instances For
∑' i, f i
is the sum of f
if it exists and is unconditionally convergent,
or 0 otherwise.
∑' i, f i
is the sum of f
if it exists and is unconditionally convergent,
or 0 otherwise.
Equations
- tsum f = if h : Summable f then if (Function.support f).Finite then finsum f else Exists.choose h else 0
Instances For
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
∏' i, f i
is the product of f
if it exists and is unconditionally convergent,
or 1 otherwise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
∑' i, f i
is the sum of f
if it exists and is unconditionally convergent,
or 0 otherwise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If a function f
is 1
outside of a finite set s
, then it HasProd
∏ b ∈ s, f b
.
If a function f
vanishes outside of a finite set s
, then it HasSum
∑ b ∈ s, f b
.