mathlib documentation

topology.algebra.infinite_sum

Infinite sum over a topological monoid #

This sum is known as unconditionally convergent, as it sums to the same value under all possible permutations. For Euclidean spaces (finite dimensional Banach spaces) this is equivalent to absolute convergence.

Note: There are summable sequences which are not unconditionally convergent! The other way holds generally, see has_sum.tendsto_sum_nat.

References #

def has_sum {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] (f : β → α) (a : α) :
Prop

Infinite sum on a topological monoid

The at_top 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 or many statements, α does not need to be a topological monoid. We only add this assumption later, for the lemmas where it is relevant.

Equations
def summable {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] (f : β → α) :
Prop

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

Equations
noncomputable def tsum {α : Type u_1} [add_comm_monoid α] [topological_space α] {β : Type u_2} (f : β → α) :
α

∑' i, f i is the sum of f it exists, or 0 otherwise

Equations
theorem summable.has_sum {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} (ha : summable f) :
has_sum f (∑' (b : β), f b)
theorem has_sum.summable {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} {a : α} (h : has_sum f a) :
theorem has_sum_zero {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] :
has_sum (λ (b : β), 0) 0

Constant zero function has sum 0

theorem has_sum_empty {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} [is_empty β] :
theorem summable_zero {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] :
summable (λ (b : β), 0)
theorem summable_empty {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} [is_empty β] :
theorem tsum_eq_zero_of_not_summable {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} (h : ¬summable f) :
∑' (b : β), f b = 0
theorem summable_congr {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f g : β → α} (hfg : ∀ (b : β), f b = g b) :
theorem summable.congr {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f g : β → α} (hf : summable f) (hfg : ∀ (b : β), f b = g b) :
theorem has_sum.has_sum_of_sum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {f : β → α} {a : α} {g : γ → α} (h_eq : ∀ (u : finset γ), ∃ (v : finset β), ∀ (v' : finset β), v v'(∃ (u' : finset γ), u u' ∑ (x : γ) in u', g x = ∑ (b : β) in v', f b)) (hf : has_sum g a) :
theorem has_sum_iff_has_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {f : β → α} {a : α} {g : γ → α} (h₁ : ∀ (u : finset γ), ∃ (v : finset β), ∀ (v' : finset β), v v'(∃ (u' : finset γ), u u' ∑ (x : γ) in u', g x = ∑ (b : β) in v', f b)) (h₂ : ∀ (v : finset β), ∃ (u : finset γ), ∀ (u' : finset γ), u u'(∃ (v' : finset β), v v' ∑ (b : β) in v', f b = ∑ (x : γ) in u', g x)) :
theorem function.injective.has_sum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {f : β → α} {a : α} {g : γ → β} (hg : function.injective g) (hf : ∀ (x : β), x set.range gf x = 0) :
has_sum (f g) a has_sum f a
theorem function.injective.summable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {f : β → α} {g : γ → β} (hg : function.injective g) (hf : ∀ (x : β), x set.range gf x = 0) :
theorem has_sum_subtype_iff_of_support_subset {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} {a : α} {s : set β} (hf : function.support f s) :
theorem has_sum_subtype_iff_indicator {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} {a : α} {s : set β} :
@[simp]
theorem has_sum_subtype_support {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} {a : α} :
theorem has_sum_fintype {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [fintype β] (f : β → α) :
has_sum f (∑ (b : β), f b)
@[protected]
theorem finset.has_sum {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] (s : finset β) (f : β → α) :
has_sum (f coe) (∑ (b : β) in s, f b)
@[protected]
theorem finset.summable {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] (s : finset β) (f : β → α) :
@[protected]
theorem set.finite.summable {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {s : set β} (hs : s.finite) (f : β → α) :
theorem has_sum_sum_of_ne_finset_zero {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} {s : finset β} (hf : ∀ (b : β), b sf b = 0) :
has_sum f (∑ (b : β) in s, f b)

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

theorem summable_of_ne_finset_zero {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} {s : finset β} (hf : ∀ (b : β), b sf b = 0) :
theorem has_sum_single {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} (b : β) (hf : ∀ (b' : β), b' bf b' = 0) :
has_sum f (f b)
theorem has_sum_ite_eq {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] (b : β) [decidable_pred (λ (_x : β), _x = b)] (a : α) :
has_sum (λ (b' : β), ite (b' = b) a 0) a
theorem equiv.has_sum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {f : β → α} {a : α} (e : γ β) :
theorem function.injective.has_sum_range_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {f : β → α} {a : α} {g : γ → β} (hg : function.injective g) :
has_sum (λ (x : (set.range g)), f x) a has_sum (f g) a
theorem equiv.summable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {f : β → α} (e : γ β) :
theorem summable.prod_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {f : β × γ → α} (hf : summable f) :
summable (λ (p : γ × β), f p.swap)
theorem equiv.has_sum_iff_of_support {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {f : β → α} {a : α} {g : γ → α} (e : (function.support f) (function.support g)) (he : ∀ (x : (function.support f)), g (e x) = f x) :
theorem has_sum_iff_has_sum_of_ne_zero_bij {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {f : β → α} {a : α} {g : γ → α} (i : (function.support g) → β) (hi : ∀ ⦃x y : (function.support g)⦄, i x = i yx = y) (hf : function.support f set.range i) (hfg : ∀ (x : (function.support g)), f (i x) = g x) :
theorem equiv.summable_iff_of_support {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {f : β → α} {g : γ → α} (e : (function.support f) (function.support g)) (he : ∀ (x : (function.support f)), g (e x) = f x) :
@[protected]
theorem has_sum.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {f : β → α} {a : α} [add_comm_monoid γ] [topological_space γ] (hf : has_sum f a) {G : Type u_4} [add_monoid_hom_class G α γ] (g : G) (hg : continuous g) :
has_sum (g f) (g a)
@[protected]
theorem summable.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {f : β → α} [add_comm_monoid γ] [topological_space γ] (hf : summable f) {G : Type u_4} [add_monoid_hom_class G α γ] (g : G) (hg : continuous g) :
theorem has_sum.tendsto_sum_nat {α : Type u_1} [add_comm_monoid α] [topological_space α] {a : α} {f : → α} (h : has_sum f a) :
filter.tendsto (λ (n : ), ∑ (i : ) in finset.range n, f i) filter.at_top (𝓝 a)

If f : ℕ → α has sum a, then the partial sums ∑_{i=0}^{n-1} f i converge to a.

theorem has_sum.unique {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} {a₁ a₂ : α} [t2_space α] :
has_sum f a₁has_sum f a₂a₁ = a₂
theorem summable.has_sum_iff_tendsto_nat {α : Type u_1} [add_comm_monoid α] [topological_space α] [t2_space α] {f : → α} {a : α} (hf : summable f) :
has_sum f a filter.tendsto (λ (n : ), ∑ (i : ) in finset.range n, f i) filter.at_top (𝓝 a)
theorem function.surjective.summable_iff_of_has_sum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] {α' : Type u_4} [add_comm_monoid α'] [topological_space α'] {e : α' → α} (hes : function.surjective e) {f : β → α} {g : γ → α'} (he : ∀ {a : α'}, has_sum f (e a) has_sum g a) :
theorem has_sum.add {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f g : β → α} {a b : α} [has_continuous_add α] (hf : has_sum f a) (hg : has_sum g b) :
has_sum (λ (b : β), f b + g b) (a + b)
theorem summable.add {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f g : β → α} [has_continuous_add α] (hf : summable f) (hg : summable g) :
summable (λ (b : β), f b + g b)
theorem has_sum_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [has_continuous_add α] {f : γ → β → α} {a : γ → α} {s : finset γ} :
(∀ (i : γ), i shas_sum (f i) (a i))has_sum (λ (b : β), ∑ (i : γ) in s, f i b) (∑ (i : γ) in s, a i)
theorem summable_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [has_continuous_add α] {f : γ → β → α} {s : finset γ} (hf : ∀ (i : γ), i ssummable (f i)) :
summable (λ (b : β), ∑ (i : γ) in s, f i b)
theorem has_sum.add_disjoint {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} {a b : α} [has_continuous_add α] {s t : set β} (hs : disjoint s t) (ha : has_sum (f coe) a) (hb : has_sum (f coe) b) :
has_sum (f coe) (a + b)
theorem has_sum.add_is_compl {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} {a b : α} [has_continuous_add α] {s t : set β} (hs : is_compl s t) (ha : has_sum (f coe) a) (hb : has_sum (f coe) b) :
has_sum f (a + b)
theorem has_sum.add_compl {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} {a b : α} [has_continuous_add α] {s : set β} (ha : has_sum (f coe) a) (hb : has_sum (f coe) b) :
has_sum f (a + b)
theorem summable.add_compl {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} [has_continuous_add α] {s : set β} (hs : summable (f coe)) (hsc : summable (f coe)) :
theorem has_sum.compl_add {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} {a b : α} [has_continuous_add α] {s : set β} (ha : has_sum (f coe) a) (hb : has_sum (f coe) b) :
has_sum f (a + b)
theorem has_sum.even_add_odd {α : Type u_1} [add_comm_monoid α] [topological_space α] {a b : α} [has_continuous_add α] {f : → α} (he : has_sum (λ (k : ), f (2 * k)) a) (ho : has_sum (λ (k : ), f (2 * k + 1)) b) :
has_sum f (a + b)
theorem summable.compl_add {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f : β → α} [has_continuous_add α] {s : set β} (hs : summable (f coe)) (hsc : summable (f coe)) :
theorem summable.even_add_odd {α : Type u_1} [add_comm_monoid α] [topological_space α] [has_continuous_add α] {f : → α} (he : summable (λ (k : ), f (2 * k))) (ho : summable (λ (k : ), f (2 * k + 1))) :
theorem has_sum.sigma {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [has_continuous_add α] [regular_space α] {γ : β → Type u_3} {f : (Σ (b : β), γ b) → α} {g : β → α} {a : α} (ha : has_sum f a) (hf : ∀ (b : β), has_sum (λ (c : γ b), f b, c⟩) (g b)) :
theorem has_sum.prod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [has_continuous_add α] [regular_space α] {f : β × γ → α} {g : β → α} {a : α} (ha : has_sum f a) (hf : ∀ (b : β), has_sum (λ (c : γ), f (b, c)) (g b)) :

If a series f on β × γ has sum a and for each b the restriction of f to {b} × γ has sum g b, then the series g has sum a.

theorem summable.sigma' {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [has_continuous_add α] [regular_space α] {γ : β → Type u_3} {f : (Σ (b : β), γ b) → α} (ha : summable f) (hf : ∀ (b : β), summable (λ (c : γ b), f b, c⟩)) :
summable (λ (b : β), ∑' (c : γ b), f b, c⟩)
theorem has_sum.sigma_of_has_sum {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [has_continuous_add α] [regular_space α] {γ : β → Type u_3} {f : (Σ (b : β), γ b) → α} {g : β → α} {a : α} (ha : has_sum g a) (hf : ∀ (b : β), has_sum (λ (c : γ b), f b, c⟩) (g b)) (hf' : summable f) :
theorem tsum_congr_subtype {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] (f : β → α) {s t : set β} (h : s = t) :
∑' (x : s), f x = ∑' (x : t), f x
theorem has_sum.tsum_eq {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] {f : β → α} {a : α} (ha : has_sum f a) :
∑' (b : β), f b = a
theorem summable.has_sum_iff {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] {f : β → α} {a : α} (h : summable f) :
has_sum f a ∑' (b : β), f b = a
@[simp]
theorem tsum_zero {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] :
∑' (b : β), 0 = 0
@[simp]
theorem tsum_empty {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] {f : β → α} [is_empty β] :
∑' (b : β), f b = 0
theorem tsum_eq_sum {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] {f : β → α} {s : finset β} (hf : ∀ (b : β), b sf b = 0) :
∑' (b : β), f b = ∑ (b : β) in s, f b
theorem tsum_congr {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] {f g : β → α} (hfg : ∀ (b : β), f b = g b) :
∑' (b : β), f b = ∑' (b : β), g b
theorem tsum_fintype {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] [fintype β] (f : β → α) :
∑' (b : β), f b = ∑ (b : β), f b
theorem tsum_bool {α : Type u_1} [add_comm_monoid α] [topological_space α] [t2_space α] (f : bool → α) :
∑' (i : bool), f i = f (to_bool false) + f (to_bool true)
@[simp]
theorem finset.tsum_subtype {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] (s : finset β) (f : β → α) :
∑' (x : {x // x s}), f x = ∑ (x : β) in s, f x
@[simp]
theorem finset.tsum_subtype' {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] (s : finset β) (f : β → α) :
∑' (x : s), f x = ∑ (x : β) in s, f x
theorem tsum_eq_single {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] {f : β → α} (b : β) (hf : ∀ (b' : β), b' bf b' = 0) :
∑' (b : β), f b = f b
@[simp]
theorem tsum_ite_eq {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] (b : β) [decidable_pred (λ (_x : β), _x = b)] (a : α) :
∑' (b' : β), ite (b' = b) a 0 = a
theorem tsum_dite_right {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] (P : Prop) [decidable P] (x : β → ¬P → α) :
∑' (b : β), dite P (λ (h : P), 0) (λ (h : ¬P), x b h) = dite P (λ (h : P), 0) (λ (h : ¬P), ∑' (b : β), x b h)
theorem tsum_dite_left {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] (P : Prop) [decidable P] (x : β → P → α) :
∑' (b : β), dite P (λ (h : P), x b h) (λ (h : ¬P), 0) = dite P (λ (h : P), ∑' (b : β), x b h) (λ (h : ¬P), 0)
theorem function.surjective.tsum_eq_tsum_of_has_sum_iff_has_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [t2_space α] {α' : Type u_4} [add_comm_monoid α'] [topological_space α'] {e : α' → α} (hes : function.surjective e) (h0 : e 0 = 0) {f : β → α} {g : γ → α'} (h : ∀ {a : α'}, has_sum f (e a) has_sum g a) :
∑' (b : β), f b = e (∑' (c : γ), g c)
theorem tsum_eq_tsum_of_has_sum_iff_has_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [t2_space α] {f : β → α} {g : γ → α} (h : ∀ {a : α}, has_sum f a has_sum g a) :
∑' (b : β), f b = ∑' (c : γ), g c
theorem equiv.tsum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [t2_space α] (j : γ β) (f : β → α) :
∑' (c : γ), f (j c) = ∑' (b : β), f b
theorem equiv.tsum_eq_tsum_of_support {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [t2_space α] {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_eq_tsum_of_ne_zero_bij {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [t2_space α] {f : β → α} {g : γ → α} (i : (function.support g) → β) (hi : ∀ ⦃x y : (function.support g)⦄, i x = i yx = y) (hf : function.support f set.range i) (hfg : ∀ (x : (function.support g)), f (i x) = g x) :
∑' (x : β), f x = ∑' (y : γ), g y
theorem tsum_subtype {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] (s : set β) (f : β → α) :
∑' (x : s), f x = ∑' (x : β), s.indicator f x
theorem tsum_add {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] {f g : β → α} [has_continuous_add α] (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} [add_comm_monoid α] [topological_space α] [t2_space α] [has_continuous_add α] {f : γ → β → α} {s : finset γ} (hf : ∀ (i : γ), i ssummable (f i)) :
∑' (b : β), ∑ (i : γ) in s, f i b = ∑ (i : γ) in s, ∑' (b : β), f i b
theorem tsum_sigma' {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] [has_continuous_add α] [regular_space α] {γ : β → Type u_3} {f : (Σ (b : β), γ b) → α} (h₁ : ∀ (b : β), summable (λ (c : γ b), f b, c⟩)) (h₂ : summable f) :
∑' (p : Σ (b : β), γ b), f p = ∑' (b : β) (c : γ b), f b, c⟩
theorem tsum_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [t2_space α] [has_continuous_add α] [regular_space α] {f : β × γ → α} (h : summable f) (h₁ : ∀ (b : β), summable (λ (c : γ), f (b, c))) :
∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)
theorem tsum_comm' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [t2_space α] [has_continuous_add α] [regular_space α] {f : β → γ → α} (h : summable (function.uncurry f)) (h₁ : ∀ (b : β), summable (f b)) (h₂ : ∀ (c : γ), summable (λ (b : β), f b c)) :
∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
theorem tsum_supr_decode₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [t2_space α] [encodable γ] [complete_lattice β] (m : β → α) (m0 : m = 0) (s : γ → β) :
∑' (i : ), m (⨆ (b : γ) (H : b encodable.decode₂ γ i), s b) = ∑' (b : γ), m (s b)

You can compute a sum over an encodably type by summing over the natural numbers and taking a supremum. This is useful for outer measures.

theorem tsum_Union_decode₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [t2_space α] [encodable γ] (m : set β → α) (m0 : m = 0) (s : γ → set β) :
∑' (i : ), m (⋃ (b : γ) (H : b encodable.decode₂ γ i), s b) = ∑' (b : γ), m (s b)

tsum_supr_decode₂ specialized to the complete lattice of sets.

Some properties about measure-like functions. These could also be functions defined on complete sublattices of sets, with the property that they are countably sub-additive. R will probably be instantiated with (≤) in all applications.

theorem rel_supr_tsum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [t2_space α] [encodable γ] [complete_lattice β] (m : β → α) (m0 : m = 0) (R : α → α → Prop) (m_supr : ∀ (s : → β), R (m (⨆ (i : ), s i)) (∑' (i : ), m (s i))) (s : γ → β) :
R (m (⨆ (b : γ), s b)) (∑' (b : γ), m (s b))

If a function is countably sub-additive then it is sub-additive on encodable types

theorem rel_supr_sum {α : Type u_1} {β : Type u_2} {δ : Type u_4} [add_comm_monoid α] [topological_space α] [t2_space α] [complete_lattice β] (m : β → α) (m0 : m = 0) (R : α → α → Prop) (m_supr : ∀ (s : → β), R (m (⨆ (i : ), s i)) (∑' (i : ), m (s i))) (s : δ → β) (t : finset δ) :
R (m (⨆ (d : δ) (H : d t), s d)) (∑ (d : δ) in t, m (s d))

If a function is countably sub-additive then it is sub-additive on finite sets

theorem rel_sup_add {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] [complete_lattice β] (m : β → α) (m0 : m = 0) (R : α → α → Prop) (m_supr : ∀ (s : → β), R (m (⨆ (i : ), s i)) (∑' (i : ), m (s i))) (s₁ s₂ : β) :
R (m (s₁ s₂)) (m s₁ + m s₂)

If a function is countably sub-additive then it is binary sub-additive

theorem tsum_add_tsum_compl {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] {f : β → α} [has_continuous_add α] {s : set β} (hs : summable (f coe)) (hsc : summable (f coe)) :
∑' (x : s), f x + ∑' (x : s), f x = ∑' (x : β), f x
theorem tsum_union_disjoint {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [topological_space α] [t2_space α] {f : β → α} [has_continuous_add α] {s t : set β} (hd : disjoint s t) (hs : summable (f coe)) (ht : summable (f coe)) :
∑' (x : (s t)), f x = ∑' (x : s), f x + ∑' (x : t), f x
theorem tsum_even_add_odd {α : Type u_1} [add_comm_monoid α] [topological_space α] [t2_space α] [has_continuous_add α] {f : → α} (he : summable (λ (k : ), f (2 * k))) (ho : summable (λ (k : ), f (2 * k + 1))) :
∑' (k : ), f (2 * k) + ∑' (k : ), f (2 * k + 1) = ∑' (k : ), f k
theorem has_sum.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [topological_space α] [add_comm_monoid γ] [topological_space γ] {f : β → α} {g : β → γ} {a : α} {b : γ} (hf : has_sum f a) (hg : has_sum g b) :
has_sum (λ (x : β), (f x, g x)) (a, b)
theorem pi.has_sum {α : Type u_1} {ι : Type u_5} {π : α → Type u_6} [Π (x : α), add_comm_monoid (π x)] [Π (x : α), topological_space (π x)] {f : ι → Π (x : α), π x} {g : Π (x : α), π x} :
has_sum f g ∀ (x : α), has_sum (λ (i : ι), f i x) (g x)
theorem pi.summable {α : Type u_1} {ι : Type u_5} {π : α → Type u_6} [Π (x : α), add_comm_monoid (π x)] [Π (x : α), topological_space (π x)] {f : ι → Π (x : α), π x} :
summable f ∀ (x : α), summable (λ (i : ι), f i x)
theorem tsum_apply {α : Type u_1} {ι : Type u_5} {π : α → Type u_6} [Π (x : α), add_comm_monoid (π x)] [Π (x : α), topological_space (π x)] [∀ (x : α), t2_space (π x)] {f : ι → Π (x : α), π x} {x : α} (hf : summable f) :
(∑' (i : ι), f i) x = ∑' (i : ι), f i x
theorem has_sum.neg {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} {a : α} (h : has_sum f a) :
has_sum (λ (b : β), -f b) (-a)
theorem summable.neg {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} (hf : summable f) :
summable (λ (b : β), -f b)
theorem summable.of_neg {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} (hf : summable (λ (b : β), -f b)) :
theorem summable_neg_iff {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} :
summable (λ (b : β), -f b) summable f
theorem has_sum.sub {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f g : β → α} {a₁ a₂ : α} (hf : has_sum f a₁) (hg : has_sum g a₂) :
has_sum (λ (b : β), f b - g b) (a₁ - a₂)
theorem summable.sub {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f g : β → α} (hf : summable f) (hg : summable g) :
summable (λ (b : β), f b - g b)
theorem summable.trans_sub {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f g : β → α} (hg : summable g) (hfg : summable (λ (b : β), f b - g b)) :
theorem summable_iff_of_summable_sub {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f g : β → α} (hfg : summable (λ (b : β), f b - g b)) :
theorem has_sum.update {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} {a₁ : α} (hf : has_sum f a₁) (b : β) [decidable_eq β] (a : α) :
has_sum (function.update f b a) (a - f b + a₁)
theorem summable.update {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} (hf : summable f) (b : β) [decidable_eq β] (a : α) :
theorem has_sum.has_sum_compl_iff {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} {a₁ a₂ : α} {s : set β} (hf : has_sum (f coe) a₁) :
has_sum (f coe) a₂ has_sum f (a₁ + a₂)
theorem has_sum.has_sum_iff_compl {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} {a₁ a₂ : α} {s : set β} (hf : has_sum (f coe) a₁) :
has_sum f a₂ has_sum (f coe) (a₂ - a₁)
theorem summable.summable_compl_iff {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} {s : set β} (hf : summable (f coe)) :
@[protected]
theorem finset.has_sum_compl_iff {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} {a : α} (s : finset β) :
has_sum (λ (x : {x // x s}), f x) a has_sum f (a + ∑ (i : β) in s, f i)
@[protected]
theorem finset.has_sum_iff_compl {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} {a : α} (s : finset β) :
has_sum f a has_sum (λ (x : {x // x s}), f x) (a - ∑ (i : β) in s, f i)
@[protected]
theorem finset.summable_compl_iff {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} (s : finset β) :
summable (λ (x : {x // x s}), f x) summable f
theorem set.finite.summable_compl_iff {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} {s : set β} (hs : s.finite) :
theorem has_sum_ite_eq_extract {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} {a : α} [decidable_eq β] (hf : has_sum f a) (b : β) :
has_sum (λ (n : β), ite (n = b) 0 (f n)) (a - f b)
theorem tsum_neg {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} [t2_space α] (hf : summable f) :
∑' (b : β), -f b = -∑' (b : β), f b
theorem tsum_sub {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f g : β → α} [t2_space α] (hf : summable f) (hg : summable g) :
∑' (b : β), (f b - g b) = ∑' (b : β), f b - ∑' (b : β), g b
theorem sum_add_tsum_compl {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} [t2_space α] {s : finset β} (hf : summable f) :
∑ (x : β) in s, f x + ∑' (x : (s)), f x = ∑' (x : β), f x
theorem tsum_ite_eq_extract {α : Type u_1} {β : Type u_2} [add_comm_group α] [topological_space α] [topological_add_group α] {f : β → α} [t2_space α] [decidable_eq β] (hf : summable f) (b : β) :
∑' (n : β), f n = f b + ∑' (n : β), ite (n = b) 0 (f n)

Let f : β → α be a sequence with summable series and let b ∈ β be an index. Lemma tsum_ite_eq_extract writes Σ f n as the sum of f b plus the series of the remaining terms.

Sums on subtypes #

If s is a finset of α, we show that the summability of f in the whole space and on the subtype univ - s are equivalent, and relate their sums. For a function defined on , we deduce the formula (∑ i in range k, f i) + (∑' i, f (i + k)) = (∑' i, f i), in sum_add_tsum_nat_add.

theorem has_sum_nat_add_iff {α : Type u_1} [add_comm_group α] [topological_space α] [topological_add_group α] {f : → α} (k : ) {a : α} :
has_sum (λ (n : ), f (n + k)) a has_sum f (a + ∑ (i : ) in finset.range k, f i)
theorem summable_nat_add_iff {α : Type u_1} [add_comm_group α] [topological_space α] [topological_add_group α] {f : → α} (k : ) :
summable (λ (n : ), f (n + k)) summable f
theorem has_sum_nat_add_iff' {α : Type u_1} [add_comm_group α] [topological_space α] [topological_add_group α] {f : → α} (k : ) {a : α} :
has_sum (λ (n : ), f (n + k)) (a - ∑ (i : ) in finset.range k, f i) has_sum f a
theorem sum_add_tsum_nat_add {α : Type u_1} [add_comm_group α] [topological_space α] [topological_add_group α] [t2_space α] {f : → α} (k : ) (h : summable f) :
∑ (i : ) in finset.range k, f i + ∑' (i : ), f (i + k) = ∑' (i : ), f i
theorem tsum_eq_zero_add {α : Type u_1} [add_comm_group α] [topological_space α] [topological_add_group α] [t2_space α] {f : → α} (hf : summable f) :
∑' (b : ), f b = f 0 + ∑' (b : ), f (b + 1)
theorem tendsto_sum_nat_add {α : Type u_1} [add_comm_group α] [topological_space α] [topological_add_group α] [t2_space α] (f : → α) :
filter.tendsto (λ (i : ), ∑' (k : ), f (k + i)) filter.at_top (𝓝 0)

For f : ℕ → α, then ∑' k, f (k + i) tends to zero. This does not require a summability assumption on f, as otherwise all sums are zero.

theorem has_sum.mul_left {α : Type u_1} {β : Type u_2} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : β → α} {a₁ : α} (a₂ : α) (h : has_sum f a₁) :
has_sum (λ (b : β), a₂ * f b) (a₂ * a₁)
theorem has_sum.mul_right {α : Type u_1} {β : Type u_2} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : β → α} {a₁ : α} (a₂ : α) (hf : has_sum f a₁) :
has_sum (λ (b : β), (f b) * a₂) (a₁ * a₂)
theorem summable.mul_left {α : Type u_1} {β : Type u_2} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : β → α} (a : α) (hf : summable f) :
summable (λ (b : β), a * f b)
theorem summable.mul_right {α : Type u_1} {β : Type u_2} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : β → α} (a : α) (hf : summable f) :
summable (λ (b : β), (f b) * a)
theorem summable.tsum_mul_left {α : Type u_1} {β : Type u_2} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : β → α} [t2_space α] (a : α) (hf : summable f) :
∑' (b : β), a * f b = a * ∑' (b : β), f b
theorem summable.tsum_mul_right {α : Type u_1} {β : Type u_2} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : β → α} [t2_space α] (a : α) (hf : summable f) :
∑' (b : β), (f b) * a = (∑' (b : β), f b) * a
theorem has_sum.const_smul {α : Type u_1} {β : Type u_2} {R : Type u_5} [monoid R] [topological_space α] [add_comm_monoid α] [distrib_mul_action R α] [has_continuous_const_smul R α] {f : β → α} {a : α} {r : R} (hf : has_sum f a) :
has_sum (λ (z : β), r f z) (r a)
theorem summable.const_smul {α : Type u_1} {β : Type u_2} {R : Type u_5} [monoid R] [topological_space α] [add_comm_monoid α] [distrib_mul_action R α] [has_continuous_const_smul R α] {f : β → α} {r : R} (hf : summable f) :
summable (λ (z : β), r f z)
theorem tsum_const_smul {α : Type u_1} {β : Type u_2} {R : Type u_5} [monoid R] [topological_space α] [add_comm_monoid α] [distrib_mul_action R α] [has_continuous_const_smul R α] {f : β → α} [t2_space α] {r : R} (hf : summable f) :
∑' (z : β), r f z = r ∑' (z : β), f z
theorem has_sum.smul_const {α : Type u_1} {β : Type u_2} {R : Type u_5} [semiring R] [topological_space R] [topological_space α] [add_comm_monoid α] [module R α] [has_continuous_smul R α] {f : β → R} {a : α} {r : R} (hf : has_sum f r) :
has_sum (λ (z : β), f z a) (r a)
theorem summable.smul_const {α : Type u_1} {β : Type u_2} {R : Type u_5} [semiring R] [topological_space R] [topological_space α] [add_comm_monoid α] [module R α] [has_continuous_smul R α] {f : β → R} {a : α} (hf : summable f) :
summable (λ (z : β), f z a)
theorem tsum_smul_const {α : Type u_1} {β : Type u_2} {R : Type u_5} [semiring R] [topological_space R] [topological_space α] [add_comm_monoid α] [module R α] [has_continuous_smul R α] {f : β → R} [t2_space α] {a : α} (hf : summable f) :
∑' (z : β), f z a = (∑' (z : β), f z) a
theorem has_sum.div_const {α : Type u_1} {β : Type u_2} [division_ring α] [topological_space α] [topological_ring α] {f : β → α} {a : α} (h : has_sum f a) (b : α) :
has_sum (λ (x : β), f x / b) (a / b)
theorem summable.div_const {α : Type u_1} {β : Type u_2} [division_ring α] [topological_space α] [topological_ring α] {f : β → α} (h : summable f) (b : α) :
summable (λ (x : β), f x / b)
theorem has_sum_mul_left_iff {α : Type u_1} {β : Type u_2} [division_ring α] [topological_space α] [topological_ring α] {f : β → α} {a₁ a₂ : α} (h : a₂ 0) :
has_sum f a₁ has_sum (λ (b : β), a₂ * f b) (a₂ * a₁)
theorem has_sum_mul_right_iff {α : Type u_1} {β : Type u_2} [division_ring α] [topological_space α] [topological_ring α] {f : β → α} {a₁ a₂ : α} (h : a₂ 0) :
has_sum f a₁ has_sum (λ (b : β), (f b) * a₂) (a₁ * a₂)
theorem summable_mul_left_iff {α : Type u_1} {β : Type u_2} [division_ring α] [topological_space α] [topological_ring α] {f : β → α} {a : α} (h : a 0) :
summable f summable (λ (b : β), a * f b)
theorem summable_mul_right_iff {α : Type u_1} {β : Type u_2} [division_ring α] [topological_space α] [topological_ring α] {f : β → α} {a : α} (h : a 0) :
summable f summable (λ (b : β), (f b) * a)
theorem tsum_mul_left {α : Type u_1} {β : Type u_2} [division_ring α] [topological_space α] [topological_ring α] {f : β → α} {a : α} [t2_space α] :
∑' (x : β), a * f x = a * ∑' (x : β), f x
theorem tsum_mul_right {α : Type u_1} {β : Type u_2} [division_ring α] [topological_space α] [topological_ring α] {f : β → α} {a : α} [t2_space α] :
∑' (x : β), (f x) * a = (∑' (x : β), f x) * a
theorem has_sum_le {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f g : β → α} {a₁ a₂ : α} (h : ∀ (b : β), f b g b) (hf : has_sum f a₁) (hg : has_sum g a₂) :
a₁ a₂
theorem has_sum_mono {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f g : β → α} {a₁ a₂ : α} (hf : has_sum f a₁) (hg : has_sum g a₂) (h : f g) :
a₁ a₂
theorem has_sum_le_of_sum_le {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} {a a₂ : α} (hf : has_sum f a) (h : ∀ (s : finset β), ∑ (b : β) in s, f b a₂) :
a a₂
theorem le_has_sum_of_le_sum {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} {a a₂ : α} (hf : has_sum f a) (h : ∀ (s : finset β), a₂ ∑ (b : β) in s, f b) :
a₂ a
theorem has_sum_le_inj {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} {a₁ a₂ : α} {g : γ → α} (i : β → γ) (hi : function.injective i) (hs : ∀ (c : γ), c set.range i0 g c) (h : ∀ (b : β), f b g (i b)) (hf : has_sum f a₁) (hg : has_sum g a₂) :
a₁ a₂
theorem tsum_le_tsum_of_inj {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} {g : γ → α} (i : β → γ) (hi : function.injective i) (hs : ∀ (c : γ), c set.range i0 g c) (h : ∀ (b : β), f b g (i b)) (hf : summable f) (hg : summable g) :
theorem sum_le_has_sum {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} {a : α} (s : finset β) (hs : ∀ (b : β), b s0 f b) (hf : has_sum f a) :
∑ (b : β) in s, f b a
theorem is_lub_has_sum {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} {a : α} (h : ∀ (b : β), 0 f b) (hf : has_sum f a) :
is_lub (set.range (λ (s : finset β), ∑ (b : β) in s, f b)) a
theorem le_has_sum {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} {a : α} (hf : has_sum f a) (b : β) (hb : ∀ (b' : β), b' b0 f b') :
f b a
theorem sum_le_tsum {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} (s : finset β) (hs : ∀ (b : β), b s0 f b) (hf : summable f) :
∑ (b : β) in s, f b ∑' (b : β), f b
theorem le_tsum {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} (hf : summable f) (b : β) (hb : ∀ (b' : β), b' b0 f b') :
f b ∑' (b : β), f b
theorem tsum_le_tsum {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f g : β → α} (h : ∀ (b : β), f b g b) (hf : summable f) (hg : summable g) :
∑' (b : β), f b ∑' (b : β), g b
theorem tsum_mono {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f g : β → α} (hf : summable f) (hg : summable g) (h : f g) :
∑' (n : β), f n ∑' (n : β), g n
theorem tsum_le_of_sum_le {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} {a₂ : α} (hf : summable f) (h : ∀ (s : finset β), ∑ (b : β) in s, f b a₂) :
∑' (b : β), f b a₂
theorem tsum_le_of_sum_le' {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} {a₂ : α} (ha₂ : 0 a₂) (h : ∀ (s : finset β), ∑ (b : β) in s, f b a₂) :
∑' (b : β), f b a₂
theorem has_sum.nonneg {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {g : β → α} {a : α} (h : ∀ (b : β), 0 g b) (ha : has_sum g a) :
0 a
theorem has_sum.nonpos {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {g : β → α} {a : α} (h : ∀ (b : β), g b 0) (ha : has_sum g a) :
a 0
theorem tsum_nonneg {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {g : β → α} (h : ∀ (b : β), 0 g b) :
0 ∑' (b : β), g b
theorem tsum_nonpos {α : Type u_1} {β : Type u_2} [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} (h : ∀ (b : β), f b 0) :
∑' (b : β), f b 0
theorem has_sum_lt {α : Type u_1} {β : Type u_2} [ordered_add_comm_group α] [topological_space α] [topological_add_group α] [order_closed_topology α] {f g : β → α} {a₁ a₂ : α} {i : β} (h : ∀ (b : β), f b g b) (hi : f i < g i) (hf : has_sum f a₁) (hg : has_sum g a₂) :
a₁ < a₂
theorem has_sum_strict_mono {α : Type u_1} {β : Type u_2} [ordered_add_comm_group α] [topological_space α] [topological_add_group α] [order_closed_topology α] {f g : β → α} {a₁ a₂ : α} (hf : has_sum f a₁) (hg : has_sum g a₂) (h : f < g) :
a₁ < a₂
theorem tsum_lt_tsum {α : Type u_1} {β : Type u_2} [ordered_add_comm_group α] [topological_space α] [topological_add_group α] [order_closed_topology α] {f g : β → α} {i : β} (h : ∀ (b : β), f b g b) (hi : f i < g i) (hf : summable f) (hg : summable g) :
∑' (n : β), f n < ∑' (n : β), g n
theorem tsum_strict_mono {α : Type u_1} {β : Type u_2} [ordered_add_comm_group α] [topological_space α] [topological_add_group α] [order_closed_topology α] {f g : β → α} (hf : summable f) (hg : summable g) (h : f < g) :
∑' (n : β), f n < ∑' (n : β), g n
theorem tsum_pos {α : Type u_1} {β : Type u_2} [ordered_add_comm_group α] [topological_space α] [topological_add_group α] [order_closed_topology α] {g : β → α} (hsum : summable g) (hg : ∀ (b : β), 0 g b) (i : β) (hi : 0 < g i) :
0 < ∑' (b : β), g b
theorem has_sum_zero_iff_of_nonneg {α : Type u_1} {β : Type u_2} [ordered_add_comm_group α] [topological_space α] [topological_add_group α] [order_closed_topology α] {f : β → α} (hf : ∀ (i : β), 0 f i) :
has_sum f 0 f = 0
theorem le_has_sum' {α : Type u_1} {β : Type u_2} [canonically_ordered_add_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} {a : α} (hf : has_sum f a) (b : β) :
f b a
theorem le_tsum' {α : Type u_1} {β : Type u_2} [canonically_ordered_add_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} (hf : summable f) (b : β) :
f b ∑' (b : β), f b
theorem has_sum_zero_iff {α : Type u_1} {β : Type u_2} [canonically_ordered_add_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} :
has_sum f 0 ∀ (x : β), f x = 0
theorem tsum_eq_zero_iff {α : Type u_1} {β : Type u_2} [canonically_ordered_add_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} (hf : summable f) :
∑' (i : β), f i = 0 ∀ (x : β), f x = 0
theorem tsum_ne_zero_iff {α : Type u_1} {β : Type u_2} [canonically_ordered_add_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} (hf : summable f) :
∑' (i : β), f i 0 ∃ (x : β), f x 0
theorem is_lub_has_sum' {α : Type u_1} {β : Type u_2} [canonically_ordered_add_monoid α] [topological_space α] [order_closed_topology α] {f : β → α} {a : α} (hf : has_sum f a) :
is_lub (set.range (λ (s : finset β), ∑ (b : β) in s, f b)) a
theorem summable_iff_cauchy_seq_finset {α : Type u_1} {β : Type u_2} [add_comm_group α] [uniform_space α] [complete_space α] {f : β → α} :
summable f cauchy_seq (λ (s : finset β), ∑ (b : β) in s, f b)

The Cauchy criterion for infinite sums, also known as the Cauchy convergence test

theorem cauchy_seq_finset_iff_vanishing {α : Type u_1} {β : Type u_2} [add_comm_group α] [uniform_space α] [uniform_add_group α] {f : β → α} :
cauchy_seq (λ (s : finset β), ∑ (b : β) in s, f b) ∀ (e : set α), e 𝓝 0(∃ (s : finset β), ∀ (t : finset β), disjoint t s∑ (b : β) in t, f b e)
theorem tendsto_tsum_compl_at_top_zero {α : Type u_1} {β : Type u_2} [add_comm_group α] [uniform_space α] [uniform_add_group α] [t1_space α] (f : β → α) :
filter.tendsto (λ (s : finset β), ∑' (b : {x // x s}), f b) filter.at_top (𝓝 0)

The sum over the complement of a finset tends to 0 when the finset grows to cover the whole space. This does not need a summability assumption, as otherwise all sums are zero.

theorem summable_iff_vanishing {α : Type u_1} {β : Type u_2} [add_comm_group α] [uniform_space α] [uniform_add_group α] {f : β → α} [complete_space α] :
summable f ∀ (e : set α), e 𝓝 0(∃ (s : finset β), ∀ (t : finset β), disjoint t s∑ (b : β) in t, f b e)
theorem summable.summable_of_eq_zero_or_self {α : Type u_1} {β : Type u_2} [add_comm_group α] [uniform_space α] [uniform_add_group α] {f g : β → α} [complete_space α] (hf : summable f) (h : ∀ (b : β), g b = 0 g b = f b) :
@[protected]
theorem summable.indicator {α : Type u_1} {β : Type u_2} [add_comm_group α] [uniform_space α] [uniform_add_group α] {f : β → α} [complete_space α] (hf : summable f) (s : set β) :
theorem summable.comp_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [uniform_space α] [uniform_add_group α] {f : β → α} [complete_space α] {i : γ → β} (hf : summable f) (hi : function.injective i) :
theorem summable.subtype {α : Type u_1} {β : Type u_2} [add_comm_group α] [uniform_space α] [uniform_add_group α] {f : β → α} [complete_space α] (hf : summable f) (s : set β) :
theorem summable_subtype_and_compl {α : Type u_1} {β : Type u_2} [add_comm_group α] [uniform_space α] [uniform_add_group α] {f : β → α} [complete_space α] {s : set β} :
summable (λ (x : s), f x) summable (λ (x : s), f x) summable f
theorem summable.sigma_factor {α : Type u_1} {β : Type u_2} [add_comm_group α] [uniform_space α] [uniform_add_group α] [complete_space α] {γ : β → Type u_3} {f : (Σ (b : β), γ b) → α} (ha : summable f) (b : β) :
summable (λ (c : γ b), f b, c⟩)
theorem summable.sigma {α : Type u_1} {β : Type u_2} [add_comm_group α] [uniform_space α] [uniform_add_group α] [complete_space α] [t1_space α] {γ : β → Type u_3} {f : (Σ (b : β), γ b) → α} (ha : summable f) :
summable (λ (b : β), ∑' (c : γ b), f b, c⟩)
theorem summable.prod_factor {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [uniform_space α] [uniform_add_group α] [complete_space α] {f : β × γ → α} (h : summable f) (b : β) :
summable (λ (c : γ), f (b, c))
theorem tsum_sigma {α : Type u_1} {β : Type u_2} [add_comm_group α] [uniform_space α] [uniform_add_group α] [complete_space α] [t1_space α] {γ : β → Type u_3} {f : (Σ (b : β), γ b) → α} (ha : summable f) :
∑' (p : Σ (b : β), γ b), f p = ∑' (b : β) (c : γ b), f b, c⟩
theorem tsum_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [uniform_space α] [uniform_add_group α] [complete_space α] [t1_space α] {f : β × γ → α} (h : summable f) :
∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)
theorem tsum_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [uniform_space α] [uniform_add_group α] [complete_space α] [t1_space α] {f : β → γ → α} (h : summable (function.uncurry f)) :
∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
theorem summable.vanishing {α : Type u_1} {G : Type u_5} [topological_space G] [add_comm_group G] [topological_add_group G] {f : α → G} (hf : summable f) ⦃e : set G⦄ (he : e 𝓝 0) :
∃ (s : finset α), ∀ (t : finset α), disjoint t s∑ (k : α) in t, f k e
theorem summable.tendsto_cofinite_zero {α : Type u_1} {G : Type u_5} [topological_space G] [add_comm_group G] [topological_add_group G] {f : α → G} (hf : summable f) :

Series divergence test: if f is a convergent series, then f x tends to zero along cofinite.

theorem summable.tendsto_top_of_pos {α : Type u_1} [linear_ordered_field α] [topological_space α] [order_topology α] {f : → α} (hf : summable f⁻¹) (hf' : ∀ (n : ), 0 < f n) :

For infinite sums taking values in a linearly ordered monoid, the existence of a least upper bound for the finite sums is a criterion for summability.

This criterion is useful when applied in a linearly ordered monoid which is also a complete or conditionally complete linear order, such as , ℝ≥0, ℝ≥0∞, because it is then easy to check the existence of a least upper bound.

theorem has_sum_of_is_lub_of_nonneg {α : Type u_1} {β : Type u_2} [linear_ordered_add_comm_monoid β] [topological_space β] [order_topology β] {f : α → β} (b : β) (h : ∀ (b : α), 0 f b) (hf : is_lub (set.range (λ (s : finset α), ∑ (a : α) in s, f a)) b) :
theorem has_sum_of_is_lub {α : Type u_1} {β : Type u_2} [canonically_linear_ordered_add_monoid β] [topological_space β] [order_topology β] {f : α → β} (b : β) (hf : is_lub (set.range (λ (s : finset α), ∑ (a : α) in s, f a)) b) :
theorem summable_abs_iff {α : Type u_1} {β : Type u_2} [linear_ordered_add_comm_group β] [uniform_space β] [uniform_add_group β] [complete_space β] {f : α → β} :
summable (λ (x : α), |f x|) summable f
theorem summable.abs {α : Type u_1} {β : Type u_2} [linear_ordered_add_comm_group β] [uniform_space β] [uniform_add_group β] [complete_space β] {f : α → β} :
summable fsummable (λ (x : α), |f x|)

Alias of summable_abs_iff.

theorem summable.of_abs {α : Type u_1} {β : Type u_2} [linear_ordered_add_comm_group β] [uniform_space β] [uniform_add_group β] [complete_space β] {f : α → β} :
summable (λ (x : α), |f x|)summable f

Alias of summable_abs_iff.

theorem finite_of_summable_const {α : Type u_1} {β : Type u_2} [linear_ordered_add_comm_group β] [archimedean β] [topological_space β] [order_closed_topology β] {b : β} (hb : 0 < b) (hf : summable (λ (a : α), b)) :
theorem cauchy_seq_of_edist_le_of_summable {α : Type u_1} [pseudo_emetric_space α] {f : → α} (d : ℝ≥0) (hf : ∀ (n : ), edist (f n) (f n.succ) (d n)) (hd : summable d) :

If the extended distance between consecutive points of a sequence is estimated by a summable series of nnreals, then the original sequence is a Cauchy sequence.

theorem cauchy_seq_of_dist_le_of_summable {α : Type u_1} [pseudo_metric_space α] {f : → α} (d : ) (hf : ∀ (n : ), dist (f n) (f n.succ) d n) (hd : summable d) :

If the distance between consecutive points of a sequence is estimated by a summable series, then the original sequence is a Cauchy sequence.

theorem cauchy_seq_of_summable_dist {α : Type u_1} [pseudo_metric_space α] {f : → α} (h : summable (λ (n : ), dist (f n) (f n.succ))) :
theorem dist_le_tsum_of_dist_le_of_tendsto {α : Type u_1} [pseudo_metric_space α] {f : → α} (d : ) (hf : ∀ (n : ), dist (f n) (f n.succ) d n) (hd : summable d) {a : α} (ha : filter.tendsto f filter.at_top (𝓝 a)) (n : ) :
dist (f n) a ∑' (m : ), d (n + m)
theorem dist_le_tsum_of_dist_le_of_tendsto₀ {α : Type u_1} [pseudo_metric_space α] {f : → α} (d : ) (hf : ∀ (n : ), dist (f n) (f n.succ) d n) (hd : summable d) {a : α} (ha : filter.tendsto f filter.at_top (𝓝 a)) :
dist (f 0) a tsum d
theorem dist_le_tsum_dist_of_tendsto {α : Type u_1} [pseudo_metric_space α] {f : → α} (h : summable (λ (n : ), dist (f n) (f n.succ))) {a : α} (ha : filter.tendsto f filter.at_top (𝓝 a)) (n : ) :
dist (f n) a ∑' (m : ), dist (f (n + m)) (f (n + m).succ)
theorem dist_le_tsum_dist_of_tendsto₀ {α : Type u_1} [pseudo_metric_space α] {f : → α} (h : summable (λ (n : ), dist (f n) (f n.succ))) {a : α} (ha : filter.tendsto f filter.at_top (𝓝 a)) :
dist (f 0) a ∑' (n : ), dist (f n) (f n.succ)

Multipliying two infinite sums #

In this section, we prove various results about (∑' x : β, f x) * (∑' y : γ, g y). Note that we always assume that the family λ x : β × γ, f x.1 * g x.2 is summable, since there is no way to deduce this from the summmabilities of f and g in general, but if you are working in a normed space, you may want to use the analogous lemmas in analysis/normed_space/basic (e.g tsum_mul_tsum_of_summable_norm).

We first establish results about arbitrary index types, β and γ, and then we specialize to β = γ = ℕ to prove the Cauchy product formula (see tsum_mul_tsum_eq_tsum_sum_antidiagonal).

Arbitrary index types #

theorem has_sum.mul_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [regular_space α] [non_unital_non_assoc_semiring α] [topological_semiring α] {f : β → α} {g : γ → α} {s t u : α} (hf : has_sum f s) (hg : has_sum g t) (hfg : has_sum (λ (x : β × γ), (f x.fst) * g x.snd) u) :
s * t = u
theorem has_sum.mul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [regular_space α] [non_unital_non_assoc_semiring α] [topological_semiring α] {f : β → α} {g : γ → α} {s t : α} (hf : has_sum f s) (hg : has_sum g t) (hfg : summable (λ (x : β × γ), (f x.fst) * g x.snd)) :
has_sum (λ (x : β × γ), (f x.fst) * g x.snd) (s * t)
theorem tsum_mul_tsum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [regular_space α] [non_unital_non_assoc_semiring α] [topological_semiring α] {f : β → α} {g : γ → α} (hf : summable f) (hg : summable g) (hfg : summable (λ (x : β × γ), (f x.fst) * g x.snd)) :
(∑' (x : β), f x) * ∑' (y : γ), g y = ∑' (z : β × γ), (f z.fst) * g z.snd

Product of two infinites sums indexed by arbitrary types. See also tsum_mul_tsum_of_summable_norm if f and g are abolutely summable.

-indexed families (Cauchy product) #

We prove two versions of the Cauchy product formula. The first one is tsum_mul_tsum_eq_tsum_sum_range, where the n-th term is a sum over finset.range (n+1) involving nat substraction. In order to avoid nat substraction, we also provide tsum_mul_tsum_eq_tsum_sum_antidiagonal, where the n-th term is a sum over all pairs (k, l) such that k+l=n, which corresponds to the finset finset.nat.antidiagonal n

theorem summable_mul_prod_iff_summable_mul_sigma_antidiagonal {α : Type u_1} [topological_space α] [non_unital_non_assoc_semiring α] {f g : → α} :
summable (λ (x : × ), (f x.fst) * g x.snd) summable (λ (x : Σ (n : ), (finset.nat.antidiagonal n)), (f (x.snd).fst) * g (x.snd).snd)
theorem summable_sum_mul_antidiagonal_of_summable_mul {α : Type u_1} [topological_space α] [non_unital_non_assoc_semiring α] [regular_space α] [topological_semiring α] {f g : → α} (h : summable (λ (x : × ), (f x.fst) * g x.snd)) :
summable (λ (n : ), ∑ (kl : × ) in finset.nat.antidiagonal n, (f kl.fst) * g kl.snd)
theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal {α : Type u_1} {f g : → α} [topological_space α] [non_unital_non_assoc_semiring α] [regular_space α] [topological_semiring α] (hf : summable f) (hg : summable g) (hfg : summable (λ (x : × ), (f x.fst) * g x.snd)) :
(∑' (n : ), f n) * ∑' (n : ), g n = ∑' (n : ), ∑ (kl : × ) in finset.nat.antidiagonal n, (f kl.fst) * g kl.snd

The Cauchy product formula for the product of two infinites sums indexed by , expressed by summing on finset.nat.antidiagonal. See also tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm if f and g are absolutely summable.

theorem summable_sum_mul_range_of_summable_mul {α : Type u_1} [topological_space α] [non_unital_non_assoc_semiring α] [regular_space α] [topological_semiring α] {f g : → α} (h : summable (λ (x : × ), (f x.fst) * g x.snd)) :
summable (λ (n : ), ∑ (k : ) in finset.range (n + 1), (f k) * g (n - k))
theorem tsum_mul_tsum_eq_tsum_sum_range {α : Type u_1} {f g : → α} [topological_space α] [non_unital_non_assoc_semiring α] [regular_space α] [topological_semiring α] (hf : summable f) (hg : summable g) (hfg : summable (λ (x : × ), (f x.fst) * g x.snd)) :
(∑' (n : ), f n) * ∑' (n : ), g n = ∑' (n : ), ∑ (k : ) in finset.range (n + 1), (f k) * g (n - k)

The Cauchy product formula for the product of two infinites sums indexed by , expressed by summing on finset.range. See also tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm if f and g are absolutely summable.