Documentation

Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

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

Instances For

    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
      class SummationFilter.NeBot {β : Type u_2} (L : SummationFilter β) :

      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.

        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
        Instances For

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

          Equations

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

          Instances
            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, bs
            def SummationFilter.map {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) (f : β γ) :

            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
            Instances For
              @[simp]
              theorem SummationFilter.map_filter {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) (f : β γ) :
              @[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 : β γ) :

              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 : γ β) :

              Pullback of a summation filter along an embedding.

              Equations
              Instances For
                @[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 : γ β) :
                instance SummationFilter.instHasSupportComap {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) [L.HasSupport] (f : γ β) :

                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 : γ β) :

                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
                Instances For

                  This instance is useful for some measure-theoretic statements.

                  @[simp]
                  theorem SummationFilter.comap_unconditional {γ : Type u_3} {β : Type u_4} (f : γ β) :

                  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
                  Instances For
                    instance SummationFilter.instNeBotConditionalOfNonemptyOfLeOfIsDirectedGe (β : Type u_2) [Preorder β] [LocallyFiniteOrder β] [Nonempty β] [IsDirected β fun (x1 x2 : β) => x1 x2] [IsDirected β fun (x1 x2 : β) => x1 x2] :
                    @[simp]

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

                    @[simp]

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

                    @[simp]

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