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.

structure SummationFilter (β : Type u_4) : Type u_4

A filter on the set of finite subsets of a type β. (Used for defining infinite topological sums and products, as limits along the given filter of partial sums / products over finsets.)

• filter : Filter (Finset β)

  The filter

class SummationFilter.LeAtTop {β : Type u_2} (L : SummationFilter β) : Prop

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.

• le_atTop : L.filter ≤ Filter.atTop

class SummationFilter.NeBot {β : Type u_2} (L : SummationFilter β) : Prop

Typeclass asserting that a summation filter is non-vacuous (if this is not satisfied, then every function is summable with every possible sum simultaneously).

• ne_bot : L.filter.NeBot

instance SummationFilter.instNeBotFinsetFilterOfNeBot {β : Type u_2} (L : SummationFilter β) [L.NeBot] : L.filter.NeBot

Makes the NeBot instance visible to the typeclass machinery.

theorem SummationFilter.neBot_or_eq_bot {β : Type u_2} (L : SummationFilter β) : L.NeBot ∨ L.filter = ⊥

def SummationFilter.support {β : Type u_2} (L : SummationFilter β) : Set β

The support of a summation filter (its lim inf, considered as a filter of sets).

Equations

• L.support = {b : β | ∀ᶠ (s : Finset β) in L.filter, b ∈ s}

theorem SummationFilter.support_eq_limsInf {β : Type u_2} (L : SummationFilter β) : L.support = (Filter.map SetLike.coe L.filter).limsInf

theorem SummationFilter.support_eq_univ_iff {β : Type u_2} {L : SummationFilter β} : L.support = Set.univ ↔ L.filter ≤ Filter.atTop

@[simp]

theorem SummationFilter.support_eq_univ {β : Type u_2} (L : SummationFilter β) [L.LeAtTop] : L.support = Set.univ

instance SummationFilter.instLeAtTopOfIsEmpty {β : Type u_2} [IsEmpty β] (L : SummationFilter β) : L.LeAtTop

theorem SummationFilter.leAtTop_of_not_NeBot {β : Type u_2} (L : SummationFilter β) (hL : ¬L.NeBot) : L.LeAtTop

instance SummationFilter.instDecidablePredMemSetSupportOfLeAtTop {β : Type u_2} (L : SummationFilter β) [L.LeAtTop] : DecidablePred fun (x : β) => x ∈ L.support

Decidability instance: useful when working with Finset sums / products.

Equations

• L.instDecidablePredMemSetSupportOfLeAtTop b = isTrue ⋯

class SummationFilter.HasSupport {β : Type u_2} (L : SummationFilter β) : Prop

Typeclass asserting that the sets in L.filter are eventually contained in L.support. This is a sufficient condition for L-summation to behave well on finitely-supported functions: every finitely-supported f is L-summable with the sum ∑ᶠ x ∈ L.support, f x (and similarly for products).

• eventually_le_support : ∀ᶠ (s : Finset β) in L.filter, ↑s ⊆ L.support

instance SummationFilter.instHasSupportOfLeAtTop {β : Type u_2} (L : SummationFilter β) [L.LeAtTop] : L.HasSupport

theorem SummationFilter.eventually_mem_or_not_mem {β : Type u_2} (L : SummationFilter β) [L.HasSupport] (b : β) : (∀ᶠ (s : Finset β) in L.filter, b ∈ s) ∨ ∀ᶠ (s : Finset β) in L.filter, b ∉ s

def SummationFilter.map {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) (f : β ↪ γ) : SummationFilter γ

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 }

@[simp]

theorem SummationFilter.map_filter {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) (f : β ↪ γ) : (L.map f).filter = Filter.map (Finset.map f) L.filter

@[simp]

theorem SummationFilter.support_map {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) [L.NeBot] (f : β ↪ γ) : (L.map f).support = ⇑f '' L.support

instance SummationFilter.instHasSupportMap {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) [L.HasSupport] (f : β ↪ γ) : (L.map f).HasSupport

If L has well-defined support, then so does its map along an embedding.

def SummationFilter.comap {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) (f : γ ↪ β) : SummationFilter γ

Pullback of a summation filter along an embedding.

Equations

• L.comap f = { filter := Filter.map (fun (s : Finset β) => s.preimage ⇑f ⋯) L.filter }

@[simp]

theorem SummationFilter.comap_filter {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) (f : γ ↪ β) : (L.comap f).filter = Filter.map (fun (s : Finset β) => s.preimage ⇑f ⋯) L.filter

@[simp]

theorem SummationFilter.support_comap {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) (f : γ ↪ β) : (L.comap f).support = ⇑f ⁻¹' L.support

instance SummationFilter.instHasSupportComap {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) [L.HasSupport] (f : γ ↪ β) : (L.comap f).HasSupport

If L has well-defined support, then so does its comap along an embedding.

instance SummationFilter.instLeAtTopComap {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) [L.LeAtTop] (f : γ ↪ β) : (L.comap f).LeAtTop

Examples of summation filters

def SummationFilter.unconditional (β : Type u_2) : SummationFilter β

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 }

@[simp]

theorem SummationFilter.unconditional_filter (β : Type u_2) : (unconditional β).filter = Filter.atTop

instance SummationFilter.instLeAtTopUnconditional (β : Type u_2) : (unconditional β).LeAtTop

instance SummationFilter.instNeBotUnconditional (β : Type u_2) : (unconditional β).NeBot

instance SummationFilter.instIsCountablyGeneratedFinsetFilterUnconditionalOfCountable (β : Type u_2) [Countable β] : (unconditional β).filter.IsCountablyGenerated

This instance is useful for some measure-theoretic statements.

@[simp]

theorem SummationFilter.comap_unconditional {γ : Type u_3} {β : Type u_4} (f : γ ↪ β) : (unconditional β).comap f = unconditional γ

The unconditional filter is preserved by comaps.

theorem SummationFilter.eq_unconditional_of_finite {β : Type u_4} [Finite β] (L : SummationFilter β) [L.LeAtTop] [L.NeBot] : L = unconditional β

If β is finite, then unconditional β is the only summation filter L on β satisfying L.LeAtTop and L.NeBot.

def SummationFilter.conditional (β : Type u_2) [Preorder β] [LocallyFiniteOrder β] : SummationFilter β

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) }

@[simp]

theorem SummationFilter.conditional_filter (β : Type u_2) [Preorder β] [LocallyFiniteOrder β] : (conditional β).filter = Filter.map (fun (p : β × β) => Finset.Icc p.1 p.2) (Filter.atBot ×ˢ Filter.atTop)

instance SummationFilter.instLeAtTopConditional (β : Type u_2) [Preorder β] [LocallyFiniteOrder β] : (conditional β).LeAtTop

instance SummationFilter.instNeBotConditionalOfNonemptyOfLeOfIsDirectedGe (β : Type u_2) [Preorder β] [LocallyFiniteOrder β] [Nonempty β] [IsDirected β fun (x1 x2 : β) => x1 ≤ x2] [IsDirected β fun (x1 x2 : β) => x1 ≥ x2] : (conditional β).NeBot

instance SummationFilter.instIsCountablyGeneratedFinsetFilterConditionalOfAtTopOfAtBot (β : Type u_2) [Preorder β] [LocallyFiniteOrder β] [Filter.atTop.IsCountablyGenerated] [Filter.atBot.IsCountablyGenerated] : (conditional β).filter.IsCountablyGenerated

@[simp]

theorem SummationFilter.conditional_filter_eq_map_Iic {γ : Type u_4} [PartialOrder γ] [LocallyFiniteOrder γ] [OrderBot γ] : (conditional γ).filter = Filter.map Finset.Iic Filter.atTop

When β has a bottom element, conditional β is given by limits over finite intervals {y | y ≤ x} as x → atTop.

@[simp]

theorem SummationFilter.conditional_filter_eq_map_Ici {γ : Type u_4} [PartialOrder γ] [LocallyFiniteOrder γ] [OrderTop γ] : (conditional γ).filter = Filter.map Finset.Ici Filter.atBot

When β has a top element, conditional β is given by limits over finite intervals {y | x ≤ y} as x → atBot.

@[simp]

theorem SummationFilter.conditional_filter_eq_map_range : (conditional ℕ).filter = Filter.map Finset.range Filter.atTop

Conditional summation over ℕ is given by limits of sums over Finset.range n as n → ∞.