Documentation

Mathlib.Topology.Algebra.InfiniteSum.Defs

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 #

def HasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : βα) (a : α) :

Infinite sum on a topological monoid

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
Instances For
    def HasProd {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : βα) (a : α) :

    Infinite product on a topological monoid

    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
    Instances For
      def Summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : βα) :

      Summable f means that f has some (infinite) sum. Use tsum to get the value.

      Equations
      Instances For
        def Multipliable {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : βα) :

        Multipliable f means that f has some (infinite) product. Use tprod to get the value.

        Equations
        Instances For
          theorem tprod_def {α : Type u_4} [CommMonoid α] [TopologicalSpace α] {β : Type u_5} (f : βα) :
          tprod f = if h : Multipliable f then if (Function.mulSupport f).Finite then finprod f else Exists.choose h else 1
          @[irreducible]
          noncomputable def tprod {α : Type u_4} [CommMonoid α] [TopologicalSpace α] {β : Type u_5} (f : βα) :
          α

          ∏' i, f i is the product of f if it exists and is unconditionally convergent, or 1 otherwise.

          Equations
          Instances For
            theorem tsum_def {α : Type u_4} [AddCommMonoid α] [TopologicalSpace α] {β : Type u_5} (f : βα) :
            tsum f = if h : Summable f then if (Function.support f).Finite then finsum f else Exists.choose h else 0

            ∑' i, f i is the sum of f if it exists and is unconditionally convergent, or 0 otherwise.

            noncomputable def tsum {α : Type u_4} [AddCommMonoid α] [TopologicalSpace α] {β : Type u_5} (f : βα) :
            α

            ∑' i, f i is the sum of f if it exists and is unconditionally convergent, or 0 otherwise.

            Equations
            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
                      theorem HasSum.summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} (h : HasSum f a) :
                      theorem HasProd.multipliable {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : βα} {a : α} (h : HasProd f a) :
                      theorem tsum_eq_zero_of_not_summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} (h : ¬Summable f) :
                      ∑' (b : β), f b = 0
                      theorem tprod_eq_one_of_not_multipliable {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : βα} (h : ¬Multipliable f) :
                      ∏' (b : β), f b = 1
                      theorem Function.Injective.hasSum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {g : γβ} (hg : Function.Injective g) (hf : xSet.range g, f x = 0) :
                      HasSum (f g) a HasSum f a
                      theorem Function.Injective.hasProd_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {g : γβ} (hg : Function.Injective g) (hf : xSet.range g, f x = 1) :
                      HasProd (f g) a HasProd f a
                      theorem hasSum_subtype_iff_of_support_subset {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {s : Set β} (hf : Function.support f s) :
                      HasSum (f Subtype.val) a HasSum f a
                      theorem hasProd_subtype_iff_of_mulSupport_subset {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {s : Set β} (hf : Function.mulSupport f s) :
                      HasProd (f Subtype.val) a HasProd f a
                      theorem hasSum_fintype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [Fintype β] (f : βα) :
                      HasSum f (∑ b : β, f b)
                      theorem hasProd_fintype {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [Fintype β] (f : βα) :
                      HasProd f (∏ b : β, f b)
                      theorem Finset.hasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : βα) :
                      HasSum (f Subtype.val) (∑ bs, f b)
                      theorem Finset.hasProd {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (s : Finset β) (f : βα) :
                      HasProd (f Subtype.val) (∏ bs, f b)
                      theorem hasSum_sum_of_ne_finset_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {s : Finset β} (hf : bs, f b = 0) :
                      HasSum f (∑ bs, f b)

                      If a function f vanishes outside of a finite set s, then it HasSum ∑ b ∈ s, f b.

                      theorem hasProd_prod_of_ne_finset_one {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : βα} {s : Finset β} (hf : bs, f b = 1) :
                      HasProd f (∏ bs, f b)

                      If a function f is 1 outside of a finite set s, then it HasProd ∏ b ∈ s, f b.

                      theorem summable_of_ne_finset_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {s : Finset β} (hf : bs, f b = 0) :
                      theorem multipliable_of_ne_finset_one {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : βα} {s : Finset β} (hf : bs, f b = 1) :
                      theorem Summable.hasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} (ha : Summable f) :
                      HasSum f (∑' (b : β), f b)
                      theorem Multipliable.hasProd {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : βα} (ha : Multipliable f) :
                      HasProd f (∏' (b : β), f b)
                      theorem HasSum.unique {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a₁ : α} {a₂ : α} [T2Space α] :
                      HasSum f a₁HasSum f a₂a₁ = a₂
                      theorem HasProd.unique {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : βα} {a₁ : α} {a₂ : α} [T2Space α] :
                      HasProd f a₁HasProd f a₂a₁ = a₂
                      theorem HasSum.tsum_eq {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} [T2Space α] (ha : HasSum f a) :
                      ∑' (b : β), f b = a
                      theorem HasProd.tprod_eq {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : βα} {a : α} [T2Space α] (ha : HasProd f a) :
                      ∏' (b : β), f b = a
                      theorem Summable.hasSum_iff {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} [T2Space α] (h : Summable f) :
                      HasSum f a ∑' (b : β), f b = a
                      theorem Multipliable.hasProd_iff {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : βα} {a : α} [T2Space α] (h : Multipliable f) :
                      HasProd f a ∏' (b : β), f b = a