Documentation

Mathlib.Topology.Algebra.InfiniteSum.Basic

Lemmas on infinite sums in topological monoids #

This file contains many simple lemmas on tsum, HasSum etc, which are placed here in order to keep the basic file of definitions as short as possible.

Results requiring a group (rather than monoid) structure on the target should go in Group.lean.

theorem hasSum_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] :
HasSum (fun (x : β) => 0) 0

Constant zero function has sum 0

theorem hasSum_empty {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} [IsEmpty β] :
HasSum f 0
theorem summable_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] :
Summable fun (x : β) => 0
theorem summable_empty {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} [IsEmpty β] :
theorem summable_congr {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {g : βα} (hfg : ∀ (b : β), f b = g b) :
theorem Summable.congr {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {g : βα} (hf : Summable f) (hfg : ∀ (b : β), f b = g b) :
theorem HasSum.hasSum_of_sum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {g : γα} (h_eq : ∀ (u : Finset γ), ∃ (v : Finset β), ∀ (v' : Finset β), v v'∃ (u' : Finset γ), u u' (Finset.sum u' fun (x : γ) => g x) = Finset.sum v' fun (b : β) => f b) (hf : HasSum g a) :
HasSum f a
theorem hasSum_iff_hasSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {g : γα} (h₁ : ∀ (u : Finset γ), ∃ (v : Finset β), ∀ (v' : Finset β), v v'∃ (u' : Finset γ), u u' (Finset.sum u' fun (x : γ) => g x) = Finset.sum v' fun (b : β) => f b) (h₂ : ∀ (v : Finset β), ∃ (u : Finset γ), ∀ (u' : Finset γ), u u'∃ (v' : Finset β), v v' (Finset.sum v' fun (b : β) => f b) = Finset.sum u' fun (x : γ) => g x) :
HasSum f a HasSum g a
theorem Function.Injective.summable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {g : γβ} (hg : Function.Injective g) (hf : xSet.range g, f x = 0) :
@[simp]
theorem hasSum_extend_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {g : βγ} (hg : Function.Injective g) :
@[simp]
theorem summable_extend_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {g : βγ} (hg : Function.Injective g) :
theorem hasSum_subtype_iff_indicator {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {s : Set β} :
HasSum (f Subtype.val) a HasSum (Set.indicator s f) a
theorem summable_subtype_iff_indicator {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {s : Set β} :
Summable (f Subtype.val) Summable (Set.indicator s f)
@[simp]
theorem hasSum_subtype_support {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} :
HasSum (f Subtype.val) a HasSum f a
theorem Finset.summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : βα) :
Summable (f Subtype.val)
theorem Set.Finite.summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {s : Set β} (hs : Set.Finite s) (f : βα) :
Summable (f Subtype.val)
theorem summable_of_finite_support {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} (h : Set.Finite (Function.support f)) :
theorem hasSum_single {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} (b : β) (hf : ∀ (b' : β), b' bf b' = 0) :
HasSum f (f b)
@[simp]
theorem hasSum_unique {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [Unique β] (f : βα) :
HasSum f (f default)
@[simp]
theorem hasSum_singleton {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (m : β) (f : βα) :
HasSum (Set.restrict {m} f) (f m)
theorem hasSum_ite_eq {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (b : β) [DecidablePred fun (x : β) => x = b] (a : α) :
HasSum (fun (b' : β) => if b' = b then a else 0) a
theorem Equiv.hasSum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} (e : γ β) :
HasSum (f e) a HasSum f a
theorem Function.Injective.hasSum_range_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {g : γβ} (hg : Function.Injective g) :
HasSum (fun (x : (Set.range g)) => f x) a HasSum (f g) a
theorem Equiv.summable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} (e : γ β) :
theorem Equiv.hasSum_iff_of_support {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {g : γα} (e : (Function.support f) (Function.support g)) (he : ∀ (x : (Function.support f)), g (e x) = f x) :
HasSum f a HasSum g a
theorem hasSum_iff_hasSum_of_ne_zero_bij {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {g : γα} (i : (Function.support g)β) (hi : Function.Injective i) (hf : Function.support f Set.range i) (hfg : ∀ (x : (Function.support g)), f (i x) = g x) :
HasSum f a HasSum g a
theorem Equiv.summable_iff_of_support {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {g : γα} (e : (Function.support f) (Function.support g)) (he : ∀ (x : (Function.support f)), g (e x) = f x) :
theorem HasSum.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} [AddCommMonoid γ] [TopologicalSpace γ] (hf : HasSum f a) {G : Type u_5} [FunLike G α γ] [AddMonoidHomClass G α γ] (g : G) (hg : Continuous g) :
HasSum (g f) (g a)
theorem Summable.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} [AddCommMonoid γ] [TopologicalSpace γ] (hf : Summable f) {G : Type u_5} [FunLike G α γ] [AddMonoidHomClass G α γ] (g : G) (hg : Continuous g) :
Summable (g f)
theorem Summable.map_iff_of_leftInverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} [AddCommMonoid γ] [TopologicalSpace γ] {G : Type u_5} {G' : Type u_6} [FunLike G α γ] [AddMonoidHomClass G α γ] [FunLike G' γ α] [AddMonoidHomClass G' γ α] (g : G) (g' : G') (hg : Continuous g) (hg' : Continuous g') (hinv : Function.LeftInverse g' g) :
theorem Summable.map_iff_of_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} [AddCommMonoid γ] [TopologicalSpace γ] {G : Type u_5} [EquivLike G α γ] [AddEquivClass G α γ] (g : G) (hg : Continuous g) (hg' : Continuous (EquivLike.inv g)) :

A special case of Summable.map_iff_of_leftInverse for convenience

theorem Function.Surjective.summable_iff_of_hasSum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {α' : Type u_5} [AddCommMonoid α'] [TopologicalSpace α'] {e : α'α} (hes : Function.Surjective e) {f : βα} {g : γα'} (he : ∀ {a : α'}, HasSum f (e a) HasSum g a) :
theorem HasSum.add {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {g : βα} {a : α} {b : α} [ContinuousAdd α] (hf : HasSum f a) (hg : HasSum g b) :
HasSum (fun (b : β) => f b + g b) (a + b)
theorem Summable.add {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {g : βα} [ContinuousAdd α] (hf : Summable f) (hg : Summable g) :
Summable fun (b : β) => f b + g b
theorem hasSum_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] {f : γβα} {a : γα} {s : Finset γ} :
(is, HasSum (f i) (a i))HasSum (fun (b : β) => Finset.sum s fun (i : γ) => f i b) (Finset.sum s fun (i : γ) => a i)
theorem summable_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] {f : γβα} {s : Finset γ} (hf : is, Summable (f i)) :
Summable fun (b : β) => Finset.sum s fun (i : γ) => f i b
theorem HasSum.add_disjoint {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {b : α} [ContinuousAdd α] {s : Set β} {t : Set β} (hs : Disjoint s t) (ha : HasSum (f Subtype.val) a) (hb : HasSum (f Subtype.val) b) :
HasSum (f Subtype.val) (a + b)
theorem hasSum_sum_disjoint {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} [ContinuousAdd α] {ι : Type u_5} (s : Finset ι) {t : ιSet β} {a : ια} (hs : Set.Pairwise (s) (Disjoint on t)) (hf : is, HasSum (f Subtype.val) (a i)) :
HasSum (f Subtype.val) (Finset.sum s fun (i : ι) => a i)
theorem HasSum.add_isCompl {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {b : α} [ContinuousAdd α] {s : Set β} {t : Set β} (hs : IsCompl s t) (ha : HasSum (f Subtype.val) a) (hb : HasSum (f Subtype.val) b) :
HasSum f (a + b)
theorem HasSum.add_compl {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {b : α} [ContinuousAdd α] {s : Set β} (ha : HasSum (f Subtype.val) a) (hb : HasSum (f Subtype.val) b) :
HasSum f (a + b)
theorem Summable.add_compl {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} [ContinuousAdd α] {s : Set β} (hs : Summable (f Subtype.val)) (hsc : Summable (f Subtype.val)) :
theorem HasSum.compl_add {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} {b : α} [ContinuousAdd α] {s : Set β} (ha : HasSum (f Subtype.val) a) (hb : HasSum (f Subtype.val) b) :
HasSum f (a + b)
theorem Summable.compl_add {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} [ContinuousAdd α] {s : Set β} (hs : Summable (f Subtype.val)) (hsc : Summable (f Subtype.val)) :
theorem HasSum.update' {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [AddCommMonoid α] [T2Space α] [ContinuousAdd α] [DecidableEq β] {f : βα} {a : α} {a' : α} (hf : HasSum f a) (b : β) (x : α) (hf' : HasSum (Function.update f b x) a') :
a + x = a' + f b

Version of HasSum.update for AddCommMonoid rather than AddCommGroup. Rather than showing that f.update has a specific sum in terms of HasSum, it gives a relationship between the sums of f and f.update given that both exist.

theorem eq_add_of_hasSum_ite {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [AddCommMonoid α] [T2Space α] [ContinuousAdd α] [DecidableEq β] {f : βα} {a : α} (hf : HasSum f a) (b : β) (a' : α) (hf' : HasSum (fun (n : β) => if n = b then 0 else f n) a') :
a = a' + f b

Version of hasSum_ite_sub_hasSum for AddCommMonoid rather than AddCommGroup. Rather than showing that the ite expression has a specific sum in terms of HasSum, it gives a relationship between the sums of f and ite (n = b) 0 (f n) given that both exist.

theorem tsum_congr_set_coe {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : βα) {s : Set β} {t : Set β} (h : s = t) :
∑' (x : s), f x = ∑' (x : t), f x
theorem tsum_congr_subtype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : βα) {P : βProp} {Q : βProp} (h : ∀ (x : β), P x Q x) :
∑' (x : { x : β // P x }), f x = ∑' (x : { x : β // Q x }), f x
theorem tsum_eq_finsum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} (hf : Set.Finite (Function.support f)) :
∑' (b : β), f b = finsum fun (b : β) => f b
theorem tsum_eq_sum' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {s : Finset β} (hf : Function.support f s) :
∑' (b : β), f b = Finset.sum s fun (b : β) => f b
theorem tsum_eq_sum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {s : Finset β} (hf : bs, f b = 0) :
∑' (b : β), f b = Finset.sum s fun (b : β) => f b
@[simp]
theorem tsum_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] :
∑' (x : β), 0 = 0
@[simp]
theorem tsum_empty {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} [IsEmpty β] :
∑' (b : β), f b = 0
theorem tsum_congr {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {g : βα} (hfg : ∀ (b : β), f b = g b) :
∑' (b : β), f b = ∑' (b : β), g b
theorem tsum_fintype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [Fintype β] (f : βα) :
∑' (b : β), f b = Finset.sum Finset.univ fun (b : β) => f b
theorem sum_eq_tsum_indicator {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : βα) (s : Finset β) :
(Finset.sum s fun (x : β) => f x) = ∑' (x : β), Set.indicator (s) f x
theorem tsum_bool {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] (f : Boolα) :
∑' (i : Bool), f i = f false + f true
theorem tsum_eq_single {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} (b : β) (hf : ∀ (b' : β), b' bf b' = 0) :
∑' (b : β), f b = f b
theorem tsum_tsum_eq_single {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] (f : βγα) (b : β) (c : γ) (hfb : ∀ (b' : β), b' bf b' c = 0) (hfc : ∀ (b' : β) (c' : γ), c' cf b' c' = 0) :
∑' (b' : β) (c' : γ), f b' c' = f b c
@[simp]
theorem tsum_ite_eq {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (b : β) [DecidablePred fun (x : β) => x = b] (a : α) :
(∑' (b' : β), if b' = b then a else 0) = a
@[simp]
theorem Finset.tsum_subtype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : βα) :
∑' (x : { x : β // x s }), f x = Finset.sum s fun (x : β) => f x
theorem Finset.tsum_subtype' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : βα) :
∑' (x : s), f x = Finset.sum s fun (x : β) => f x
@[simp]
theorem tsum_singleton {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (b : β) (f : βα) :
∑' (x : {b}), f x = f b
theorem Function.Injective.tsum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {g : γβ} (hg : Function.Injective g) {f : βα} (hf : Function.support f Set.range g) :
∑' (c : γ), f (g c) = ∑' (b : β), f b
theorem Equiv.tsum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] (e : γ β) (f : βα) :
∑' (c : γ), f (e c) = ∑' (b : β), f b

tsum on subsets - part 1 #

theorem tsum_subtype_eq_of_support_subset {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {s : Set β} (hs : Function.support f s) :
∑' (x : s), f x = ∑' (x : β), f x
theorem tsum_subtype_support {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : βα) :
∑' (x : (Function.support f)), f x = ∑' (x : β), f x
theorem tsum_subtype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Set β) (f : βα) :
∑' (x : s), f x = ∑' (x : β), Set.indicator s f x
@[simp]
theorem tsum_univ {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : βα) :
∑' (x : Set.univ), f x = ∑' (x : β), f x
theorem tsum_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {g : γβ} (f : βα) {s : Set γ} (hg : Set.InjOn g s) :
∑' (x : (g '' s)), f x = ∑' (x : s), f (g x)
theorem tsum_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {g : γβ} (f : βα) (hg : Function.Injective g) :
∑' (x : (Set.range g)), f x = ∑' (x : γ), f (g x)
theorem tsum_setElem_eq_tsum_setElem_diff {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} (s : Set β) (t : Set β) (hf₀ : bt, f b = 0) :
∑' (a : s), f a = ∑' (a : (s \ t)), f a

If f b = 0 for all b ∈ t, then the sum over f a with a ∈ s is the same as the sum over f a with a ∈ s ∖ t.

theorem tsum_eq_tsum_diff_singleton {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} (s : Set β) {b : β} (hf₀ : f b = 0) :
∑' (a : s), f a = ∑' (a : (s \ {b})), f a

If f b = 0, then the sum over f a with a ∈ s is the same as the sum over f a for a ∈ s ∖ {b}.

theorem tsum_eq_tsum_of_ne_zero_bij {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {g : γα} (i : (Function.support g)β) (hi : Function.Injective i) (hf : Function.support f Set.range i) (hfg : ∀ (x : (Function.support g)), f (i x) = g x) :
∑' (x : β), f x = ∑' (y : γ), g y
theorem Equiv.tsum_eq_tsum_of_support {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {g : γα} (e : (Function.support f) (Function.support g)) (he : ∀ (x : (Function.support f)), g (e x) = f x) :
∑' (x : β), f x = ∑' (y : γ), g y
theorem tsum_dite_right {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (P : Prop) [Decidable P] (x : β¬Pα) :
(∑' (b : β), if h : P then 0 else x b h) = if h : P then 0 else ∑' (b : β), x b h
theorem tsum_dite_left {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (P : Prop) [Decidable P] (x : βPα) :
(∑' (b : β), if h : P then x b h else 0) = if h : P then ∑' (b : β), x b h else 0
@[simp]
theorem tsum_extend_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {γ : Type u_5} {g : γβ} (hg : Function.Injective g) (f : γα) :
∑' (y : β), Function.extend g f 0 y = ∑' (x : γ), f x
theorem Function.Surjective.tsum_eq_tsum_of_hasSum_iff_hasSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] {α' : Type u_5} [AddCommMonoid α'] [TopologicalSpace α'] {e : α'α} (hes : Function.Surjective e) (h0 : e 0 = 0) {f : βα} {g : γα'} (h : ∀ {a : α'}, HasSum f (e a) HasSum g a) :
∑' (b : β), f b = e (∑' (c : γ), g c)
theorem tsum_eq_tsum_of_hasSum_iff_hasSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] {f : βα} {g : γα} (h : ∀ {a : α}, HasSum f a HasSum g a) :
∑' (b : β), f b = ∑' (c : γ), g c
theorem tsum_add {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {g : βα} [T2Space α] [ContinuousAdd α] (hf : Summable f) (hg : Summable g) :
∑' (b : β), (f b + g b) = ∑' (b : β), f b + ∑' (b : β), g b
theorem tsum_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] [ContinuousAdd α] {f : γβα} {s : Finset γ} (hf : is, Summable (f i)) :
(∑' (b : β), Finset.sum s fun (i : γ) => f i b) = Finset.sum s fun (i : γ) => ∑' (b : β), f i b
theorem tsum_eq_add_tsum_ite' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] [ContinuousAdd α] [DecidableEq β] {f : βα} (b : β) (hf : Summable (Function.update f b 0)) :
∑' (x : β), f x = f b + ∑' (x : β), if x = b then 0 else f x

Version of tsum_eq_add_tsum_ite for AddCommMonoid rather than AddCommGroup. Requires a different convergence assumption involving Function.update.

theorem tsum_add_tsum_compl {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} [T2Space α] [ContinuousAdd α] {s : Set β} (hs : Summable (f Subtype.val)) (hsc : Summable (f Subtype.val)) :
∑' (x : s), f x + ∑' (x : s), f x = ∑' (x : β), f x
theorem tsum_union_disjoint {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} [T2Space α] [ContinuousAdd α] {s : Set β} {t : Set β} (hd : Disjoint s t) (hs : Summable (f Subtype.val)) (ht : Summable (f Subtype.val)) :
∑' (x : (s t)), f x = ∑' (x : s), f x + ∑' (x : t), f x
theorem tsum_finset_bUnion_disjoint {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} [T2Space α] [ContinuousAdd α] {ι : Type u_5} {s : Finset ι} {t : ιSet β} (hd : Set.Pairwise (s) (Disjoint on t)) (hf : is, Summable (f Subtype.val)) :
∑' (x : (⋃ i ∈ s, t i)), f x = Finset.sum s fun (i : ι) => ∑' (x : (t i)), f x