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)

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

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

• HasSum f a = Filter.Tendsto (fun (s : Finset β) => ∑ b ∈ s, f b) Filter.atTop (nhds a)

def HasProd {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : β → α) (a : α) : Prop

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

• HasProd f a = Filter.Tendsto (fun (s : Finset β) => ∏ b ∈ s, f b) Filter.atTop (nhds a)

def Summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) : Prop

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

Equations

• Summable f = ∃ (a : α), HasSum f a

def Multipliable {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : β → α) : Prop

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

Equations

• Multipliable f = ∃ (a : α), HasProd f a

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

• @tprod = wrapped✝.1

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

• @tsum = wrapped✝.1

def «term∏'_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def «term∏'_,_» : Lean.ParserDescr

∏' 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.

def «term∑'_,_» : Lean.ParserDescr

∑' 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.

def «term∑'_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

theorem HasSum.summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} (h : HasSum f a) : Summable f

theorem HasProd.multipliable {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} (h : HasProd f a) : Multipliable f

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 : ∀ x ∉ Set.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 : ∀ x ∉ Set.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) (∑ b ∈ s, f b)

theorem Finset.hasProd {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) : HasProd (f ∘ Subtype.val) (∏ b ∈ s, f b)

theorem hasSum_sum_of_ne_finset_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {s : Finset β} (hf : ∀ b ∉ s, f b = 0) : HasSum f (∑ b ∈ s, 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 : ∀ b ∉ s, f b = 1) : HasProd f (∏ b ∈ s, 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 : ∀ b ∉ s, f b = 0) : Summable f

theorem multipliable_of_ne_finset_one {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {s : Finset β} (hf : ∀ b ∉ s, f b = 1) : Multipliable f

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