Summation filters #
We define a SummationFilter
on β
to be a filter on the finite subsets of β
. These are used
in defining summability: if L
is a summation filter, we define the L
-sum of f
to be the
limit along L
of the sums over finsets (if this limit exists). This file only develops the basic
machinery of summation filters - the key definitions HasSum
, tsum
and summable
(and their
product variants) are in the file Mathlib.Topology.Algebra.InfiniteSum.Defs
.
Typeclass asserting that a summation filter L
is consistent with unconditional summation,
so that any unconditionally-summable function is L
-summable with the same sum.
Instances
Typeclass asserting that a summation filter is non-vacuous (if this is not satisfied, then every function is summable with every possible sum simultaneously).
Instances
Makes the NeBot
instance visible to the typeclass machinery.
Decidability instance: useful when working with Finset
sums / products.
Equations
Pushforward of a summation filter along an embedding.
(We define this only for embeddings, rather than arbitrary maps, since this is the only case needed
for the intended applications, and this avoids requiring a DecidableEq
instance on γ
.)
Equations
- L.map f = { filter := Filter.map (Finset.map f) L.filter }
Instances For
If L
has well-defined support, then so does its map along an embedding.
Pullback of a summation filter along an embedding.
Instances For
If L
has well-defined support, then so does its comap along an embedding.
Examples of summation filters #
Unconditional summation: a function on β
is said to be unconditionally summable if its
partial sums over finite subsets converge with respect to the atTop
filter.
Equations
- SummationFilter.unconditional β = { filter := Filter.atTop }
Instances For
This instance is useful for some measure-theoretic statements.
The unconditional filter is preserved by comaps.
If β
is finite, then unconditional β
is the only summation filter L
on β
satisfying
L.LeAtTop
and L.NeBot
.
Conditional summation, for ordered types β
such that closed intervals [x, y]
are
finite: this corresponds to limits of finite sums over larger and larger intervals.
Equations
- SummationFilter.conditional β = { filter := Filter.map (fun (p : β × β) => Finset.Icc p.1 p.2) (Filter.atBot ×ˢ Filter.atTop) }
Instances For
When β
has a bottom element, conditional β
is given by limits over finite intervals
{y | y ≤ x}
as x → atTop
.
When β
has a top element, conditional β
is given by limits over finite intervals
{y | x ≤ y}
as x → atBot
.
Conditional summation over ℕ
is given by limits of sums over Finset.range n
as n → ∞
.