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 HasSum.tendsto_sum_nat.

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

• HasSum f a = Filter.Tendsto (fun s => Finset.sum s fun b => 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

@[irreducible]

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

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

Equations

• @tsum = wrapped✝.1

theorem tsum_def {α : Type u_5} [AddCommMonoid α] [TopologicalSpace α] {β : Type u_6} (f : β → α) : tsum f = if h : Summable f then if Set.Finite (Function.support f) then finsum f else Classical.choose h else 0

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

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 it exists, or 0 otherwise.

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 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 β] : Summable 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 summable_congr {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} (hfg : ∀ (b : β), f b = g b) : Summable f ↔ Summable g

theorem Summable.congr {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} (hf : Summable f) (hfg : ∀ (b : β), f b = g b) : Summable g

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, ∀ (v' : Finset β), v ⊆ v' → ∃ u', 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, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ (Finset.sum u' fun x => g x) = Finset.sum v' fun b => f b) (h₂ : ∀ (v : Finset β), ∃ u, ∀ (u' : Finset γ), u ⊆ u' → ∃ v', 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.hasSum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → β} (hg : Function.Injective g) (hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 0) : HasSum (f ∘ g) a ↔ HasSum f a

theorem Function.Injective.summable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : γ → β} (hg : Function.Injective g) (hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 0) : Summable (f ∘ g) ↔ Summable f

@[simp]

theorem hasSum_extend_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : β → γ} (hg : Function.Injective g) : HasSum (Function.extend g f 0) a ↔ HasSum f a

@[simp]

theorem summable_extend_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → γ} (hg : Function.Injective g) : Summable (Function.extend g f 0) ↔ Summable f

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 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 hasSum_fintype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [Fintype β] (f : β → α) : HasSum f (Finset.sum Finset.univ fun b => f b)

theorem Finset.hasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) : HasSum (f ∘ Subtype.val) (Finset.sum s fun b => f b)

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 hasSum_sum_of_ne_finset_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {s : Finset β} (hf : ∀ (b : β), ¬b ∈ s → f b = 0) : HasSum f (Finset.sum s fun b => f b)

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

theorem summable_of_ne_finset_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {s : Finset β} (hf : ∀ (b : β), ¬b ∈ s → f b = 0) : Summable f

theorem summable_of_finite_support {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (h : Set.Finite (Function.support f)) : Summable f

theorem Summable.hasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (ha : Summable f) : HasSum f (∑' (b : β), f b)

theorem hasSum_single {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (b : β) (hf : ∀ (b' : β), b' ≠ b → f b' = 0) : HasSum f (f b)

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 hasSum_pi_single {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [DecidableEq β] (b : β) (a : α) : HasSum (Pi.single b a) 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 => f ↑x) a ↔ HasSum (f ∘ g) a

theorem Equiv.summable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (e : γ ≃ β) : Summable (f ∘ ↑e) ↔ Summable f

theorem Summable.prod_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β × γ → α} (hf : Summable f) : Summable fun p => f (Prod.swap p)

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 : ∀ ⦃x y : ↑(Function.support g)⦄, i x = i y → ↑x = ↑y) (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) : Summable f ↔ Summable g

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} [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} [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} [AddMonoidHomClass G α γ] [AddMonoidHomClass G' γ α] (g : G) (g' : G') (hg : Continuous ↑g) (hg' : Continuous ↑g') (hinv : Function.LeftInverse ↑g' ↑g) : Summable (↑g ∘ f) ↔ Summable f

theorem Summable.map_iff_of_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [AddCommMonoid γ] [TopologicalSpace γ] {G : Type u_5} [AddEquivClass G α γ] (g : G) (hg : Continuous ↑g) (hg' : Continuous (EquivLike.inv g)) : Summable (↑g ∘ f) ↔ Summable f

A special case of Summable.map_iff_of_leftInverse for convenience

theorem HasSum.tendsto_sum_nat {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] {a : α} {f : ℕ → α} (h : HasSum f a) : Filter.Tendsto (fun n => Finset.sum (Finset.range n) fun i => f i) Filter.atTop (nhds a)

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

theorem HasSum.unique {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a₁ : α} {a₂ : α} [T2Space α] : HasSum f a₁ → HasSum f a₂ → a₁ = a₂

theorem Summable.hasSum_iff_tendsto_nat {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] {f : ℕ → α} {a : α} (hf : Summable f) : HasSum f a ↔ Filter.Tendsto (fun n => Finset.sum (Finset.range n) fun i => f i) Filter.atTop (nhds a)

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) : Summable f ↔ Summable g

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 γ} : (∀ (i : γ), i ∈ s → 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 : ∀ (i : γ), i ∈ s → 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 : ∀ (i : ι), i ∈ s → 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)) : Summable f

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 HasSum.even_add_odd {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] {a : α} {b : α} [ContinuousAdd α] {f : ℕ → α} (he : HasSum (fun k => f (2 * k)) a) (ho : HasSum (fun k => f (2 * k + 1)) 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)) : Summable f

theorem Summable.even_add_odd {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] {f : ℕ → α} (he : Summable fun k => f (2 * k)) (ho : Summable fun k => f (2 * k + 1)) : Summable f

theorem HasSum.sigma {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [RegularSpace α] {γ : β → Type u_5} {f : (b : β) × γ b → α} {g : β → α} {a : α} (ha : HasSum f a) (hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)) : HasSum g a

theorem HasSum.prod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [RegularSpace α] {f : β × γ → α} {g : β → α} {a : α} (ha : HasSum f a) (hf : ∀ (b : β), HasSum (fun c => f (b, c)) (g b)) : HasSum g a

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} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [RegularSpace α] {γ : β → Type u_5} {f : (b : β) × γ b → α} (ha : Summable f) (hf : ∀ (b : β), Summable fun c => f { fst := b, snd := c }) : Summable fun b => ∑' (c : γ b), f { fst := b, snd := c }

theorem HasSum.sigma_of_hasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [T3Space α] {γ : β → Type u_5} {f : (b : β) × γ b → α} {g : β → α} {a : α} (ha : HasSum g a) (hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)) (hf' : Summable f) : HasSum f a

theorem HasSum.update' {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [AddCommMonoid α] [T2Space α] [ContinuousAdd α] {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 α] {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_subtype {α : 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_eq_finsum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (hf : Set.Finite (Function.support f)) : ∑' (b : β), f b = ∑ᶠ (b : β), f b

theorem tsum_eq_sum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {s : Finset β} (hf : ∀ (b : β), ¬b ∈ s → 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' ≠ b → f 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' ≠ b → f b' c = 0) (hfc : ∀ (b' : β) (c' : γ), c' ≠ c → f 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 tsum_pi_single {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [DecidableEq β] (b : β) (a : α) : ∑' (b' : β), Pi.single b a b' = 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 HasSum.tsum_eq {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} [T2Space α] (ha : HasSum 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 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

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 Equiv.tsum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] (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} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] {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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] {g : γ → α} (i : ↑(Function.support g) → β) (hi : ∀ ⦃x y : ↑(Function.support g)⦄, i x = i y → ↑x = ↑y) (hf : Function.support f ⊆ Set.range i) (hfg : ∀ (x : ↑(Function.support g)), f (i x) = g ↑x) : ∑' (x : β), f x = ∑' (y : γ), g y

tsum on subsets

theorem tsum_subtype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] (s : Set β) (f : β → α) : ∑' (x : ↑s), f ↑x = ∑' (x : β), Set.indicator s f x

theorem tsum_subtype_eq_of_support_subset {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] {f : β → α} {s : Set β} (hs : Function.support f ⊆ s) : ∑' (x : ↑s), f ↑x = ∑' (x : β), f x

@[simp]

theorem tsum_univ {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] (f : β → α) : ∑' (x : ↑Set.univ), f ↑x = ∑' (x : β), f x

theorem tsum_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] {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 α] [T2Space α] {g : γ → β} (f : β → α) (hg : Function.Injective g) : ∑' (x : ↑(Set.range g)), f ↑x = ∑' (x : γ), f (g x)

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 : ∀ (i : γ), i ∈ s → 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 α] {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_sigma' {β : Type u_2} {δ : Type u_4} [AddCommMonoid δ] [TopologicalSpace δ] [T3Space δ] [ContinuousAdd δ] {γ : β → Type u_5} {f : (b : β) × γ b → δ} (h₁ : ∀ (b : β), Summable fun c => f { fst := b, snd := c }) (h₂ : Summable f) : ∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f { fst := b, snd := c }

theorem tsum_prod' {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [AddCommMonoid δ] [TopologicalSpace δ] [T3Space δ] [ContinuousAdd δ] {f : β × γ → δ} (h : Summable f) (h₁ : ∀ (b : β), Summable fun c => f (b, c)) : ∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)

theorem tsum_comm' {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [AddCommMonoid δ] [TopologicalSpace δ] [T3Space δ] [ContinuousAdd δ] {f : β → γ → δ} (h : Summable (Function.uncurry f)) (h₁ : ∀ (b : β), Summable (f b)) (h₂ : ∀ (c : γ), Summable fun b => f b c) : ∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c

theorem tsum_iSup_decode₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] [Encodable γ] [CompleteLattice β] (m : β → α) (m0 : m ⊥ = 0) (s : γ → β) : ∑' (i : ℕ), m (⨆ (b : γ) (_ : 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_iUnion_decode₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] [Encodable γ] (m : Set β → α) (m0 : m ∅ = 0) (s : γ → Set β) : ∑' (i : ℕ), m (⋃ (b : γ) (_ : b ∈ Encodable.decode₂ γ i), s b) = ∑' (b : γ), m (s b)

tsum_iSup_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_iSup_tsum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] [Countable γ] [CompleteLattice β] (m : β → α) (m0 : m ⊥ = 0) (R : α → α → Prop) (m_iSup : (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 countable types

theorem rel_iSup_sum {α : Type u_1} {β : Type u_2} {δ : Type u_4} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] [CompleteLattice β] (m : β → α) (m0 : m ⊥ = 0) (R : α → α → Prop) (m_iSup : (s : ℕ → β) → R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))) (s : δ → β) (t : Finset δ) : R (m (⨆ (d : δ) (_ : d ∈ t), s d)) (Finset.sum t fun d => 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} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] [CompleteLattice β] (m : β → α) (m0 : m ⊥ = 0) (R : α → α → Prop) (m_iSup : (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} [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 : ∀ (i : ι), i ∈ s → Summable (f ∘ Subtype.val)) : ∑' (x : ↑(⋃ (i : ι) (_ : i ∈ s), t i)), f ↑x = Finset.sum s fun i => ∑' (x : ↑(t i)), f ↑x

theorem tsum_even_add_odd {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] [ContinuousAdd α] {f : ℕ → α} (he : Summable fun k => f (2 * k)) (ho : Summable fun k => f (2 * k + 1)) : ∑' (k : ℕ), f (2 * k) + ∑' (k : ℕ), f (2 * k + 1) = ∑' (k : ℕ), f k

theorem HasSum.neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {a : α} (h : HasSum f a) : HasSum (fun b => -f b) (-a)

theorem Summable.neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} (hf : Summable f) : Summable fun b => -f b

theorem Summable.of_neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} (hf : Summable fun b => -f b) : Summable f

theorem summable_neg_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} : (Summable fun b => -f b) ↔ Summable f

theorem HasSum.sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {g : β → α} {a₁ : α} {a₂ : α} (hf : HasSum f a₁) (hg : HasSum g a₂) : HasSum (fun b => f b - g b) (a₁ - a₂)

theorem Summable.sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {g : β → α} (hf : Summable f) (hg : Summable g) : Summable fun b => f b - g b

theorem Summable.trans_sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {g : β → α} (hg : Summable g) (hfg : Summable fun b => f b - g b) : Summable f

theorem summable_iff_of_summable_sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {g : β → α} (hfg : Summable fun b => f b - g b) : Summable f ↔ Summable g

theorem HasSum.update {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {a₁ : α} (hf : HasSum f a₁) (b : β) [DecidableEq β] (a : α) : HasSum (Function.update f b a) (a - f b + a₁)

theorem Summable.update {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} (hf : Summable f) (b : β) [DecidableEq β] (a : α) : Summable (Function.update f b a)

theorem HasSum.hasSum_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {a₁ : α} {a₂ : α} {s : Set β} (hf : HasSum (f ∘ Subtype.val) a₁) : HasSum (f ∘ Subtype.val) a₂ ↔ HasSum f (a₁ + a₂)

theorem HasSum.hasSum_iff_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {a₁ : α} {a₂ : α} {s : Set β} (hf : HasSum (f ∘ Subtype.val) a₁) : HasSum f a₂ ↔ HasSum (f ∘ Subtype.val) (a₂ - a₁)

theorem Summable.summable_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {s : Set β} (hf : Summable (f ∘ Subtype.val)) : Summable (f ∘ Subtype.val) ↔ Summable f

theorem Finset.hasSum_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {a : α} (s : Finset β) : HasSum (fun x => f ↑x) a ↔ HasSum f (a + Finset.sum s fun i => f i)

theorem Finset.hasSum_iff_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {a : α} (s : Finset β) : HasSum f a ↔ HasSum (fun x => f ↑x) (a - Finset.sum s fun i => f i)

theorem Finset.summable_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} (s : Finset β) : (Summable fun x => f ↑x) ↔ Summable f

theorem Set.Finite.summable_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {s : Set β} (hs : Set.Finite s) : Summable (f ∘ Subtype.val) ↔ Summable f

theorem hasSum_ite_sub_hasSum {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {a : α} [DecidableEq β] (hf : HasSum f a) (b : β) : HasSum (fun n => if n = b then 0 else f n) (a - f b)

theorem tsum_neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} [T2Space α] : ∑' (b : β), -f b = -∑' (b : β), f b

theorem tsum_sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} {g : β → α} [T2Space α] (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} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} [T2Space α] {s : Finset β} (hf : Summable f) : (Finset.sum s fun x => f x) + ∑' (x : ↑(↑s)ᶜ), f ↑x = ∑' (x : β), f x

theorem tsum_eq_add_tsum_ite {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : β → α} [T2Space α] [DecidableEq β] (hf : Summable f) (b : β) : ∑' (n : β), f n = f b + ∑' (n : β), if n = b then 0 else f n

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

Sums on nat

We show the formula ∑ i in range k, f i + ∑' i, f (i + k) = ∑' i, f i, in sum_add_tsum_nat_add, as well as several results relating sums on ℕ and ℤ.

theorem hasSum_nat_add_iff {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : ℕ → α} (k : ℕ) {a : α} : HasSum (fun n => f (n + k)) a ↔ HasSum f (a + Finset.sum (Finset.range k) fun i => f i)

theorem summable_nat_add_iff {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : ℕ → α} (k : ℕ) : (Summable fun n => f (n + k)) ↔ Summable f

theorem hasSum_nat_add_iff' {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : ℕ → α} (k : ℕ) {a : α} : HasSum (fun n => f (n + k)) (a - Finset.sum (Finset.range k) fun i => f i) ↔ HasSum f a

theorem HasSum.sum_range_add {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {f : ℕ → M} {k : ℕ} {a : M} (h : HasSum (fun n => f (n + k)) a) : HasSum f ((Finset.sum (Finset.range k) fun i => f i) + a)

theorem sum_add_tsum_nat_add' {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : ℕ → M} {k : ℕ} (h : Summable fun n => f (n + k)) : (Finset.sum (Finset.range k) fun i => f i) + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i

theorem sum_add_tsum_nat_add {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [T2Space α] {f : ℕ → α} (k : ℕ) (h : Summable f) : (Finset.sum (Finset.range k) fun i => f i) + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i

theorem tsum_eq_zero_add' {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : ℕ → M} (hf : Summable fun n => f (n + 1)) : ∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)

theorem tsum_eq_zero_add {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [T2Space α] {f : ℕ → α} (hf : Summable f) : ∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)

theorem tendsto_sum_nat_add {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [T2Space α] (f : ℕ → α) : Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 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 HasSum.int_rec {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {a : α} {b : α} {f : ℕ → α} {g : ℕ → α} (hf : HasSum f a) (hg : HasSum g b) : HasSum (Int.rec f g) (a + b)

If f₀, f₁, f₂, ... and g₀, g₁, g₂, ... are both convergent then so is the ℤ-indexed sequence: ..., g₂, g₁, g₀, f₀, f₁, f₂, ....

theorem HasSum.nonneg_add_neg {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {a : α} {b : α} {f : ℤ → α} (hnonneg : HasSum (fun n => f ↑n) a) (hneg : HasSum (fun n => f (-↑(Nat.succ n))) b) : HasSum f (a + b)

theorem HasSum.pos_add_zero_add_neg {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {a : α} {b : α} {f : ℤ → α} (hpos : HasSum (fun n => f (↑n + 1)) a) (hneg : HasSum (fun n => f (-↑(Nat.succ n))) b) : HasSum f (a + f 0 + b)

theorem summable_int_of_summable_nat {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : ℤ → α} (hp : Summable fun n => f ↑n) (hn : Summable fun n => f (-↑n)) : Summable f

theorem HasSum.sum_nat_of_sum_int {α : Type u_5} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] {a : α} {f : ℤ → α} (hf : HasSum f a) : HasSum (fun n => f ↑n + f (-↑n)) (a + f 0)

theorem summable_iff_cauchySeq_finset {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [CompleteSpace α] {f : β → α} : Summable f ↔ CauchySeq fun s => Finset.sum s fun b => f b

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

theorem cauchySeq_finset_iff_vanishing {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : β → α} : (CauchySeq fun s => Finset.sum s fun b => f b) ↔ ∀ (e : Set α), e ∈ nhds 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → (Finset.sum t fun b => f b) ∈ e

theorem tendsto_tsum_compl_atTop_zero {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] (f : β → α) : Filter.Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) Filter.atTop (nhds 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} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : β → α} [CompleteSpace α] : Summable f ↔ ∀ (e : Set α), e ∈ nhds 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → (Finset.sum t fun b => f b) ∈ e

theorem Summable.summable_of_eq_zero_or_self {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : β → α} {g : β → α} [CompleteSpace α] (hf : Summable f) (h : ∀ (b : β), g b = 0 ∨ g b = f b) : Summable g

theorem Summable.indicator {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : β → α} [CompleteSpace α] (hf : Summable f) (s : Set β) : Summable (Set.indicator s f)

theorem Summable.comp_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : β → α} [CompleteSpace α] {i : γ → β} (hf : Summable f) (hi : Function.Injective i) : Summable (f ∘ i)

theorem Summable.subtype {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : β → α} [CompleteSpace α] (hf : Summable f) (s : Set β) : Summable (f ∘ Subtype.val)

theorem summable_subtype_and_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : β → α} [CompleteSpace α] {s : Set β} : ((Summable fun x => f ↑x) ∧ Summable fun x => f ↑x) ↔ Summable f

theorem Summable.sigma_factor {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {γ : β → Type u_5} {f : (b : β) × γ b → α} (ha : Summable f) (b : β) : Summable fun c => f { fst := b, snd := c }

theorem Summable.sigma {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {γ : β → Type u_5} {f : (b : β) × γ b → α} (ha : Summable f) : Summable fun b => ∑' (c : γ b), f { fst := b, snd := c }

theorem Summable.prod_factor {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {f : β × γ → α} (h : Summable f) (b : β) : Summable fun c => f (b, c)

theorem tsum_sigma {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] [T0Space α] {γ : β → Type u_5} {f : (b : β) × γ b → α} (ha : Summable f) : ∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f { fst := b, snd := c }

theorem tsum_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] [T0Space α] {f : β × γ → α} (h : Summable f) : ∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)

theorem tsum_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] [T0Space α] {f : β → γ → α} (h : Summable (Function.uncurry f)) : ∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c

theorem tsum_subtype_add_tsum_subtype_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] [T2Space α] {f : β → α} (hf : Summable f) (s : Set β) : ∑' (x : ↑s), f ↑x + ∑' (x : ↑sᶜ), f ↑x = ∑' (x : β), f x

theorem sum_add_tsum_subtype_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] [T2Space α] {f : β → α} (hf : Summable f) (s : Finset β) : (Finset.sum s fun x => f x) + ∑' (x : { x // ¬x ∈ s }), f ↑x = ∑' (x : β), f x

theorem Summable.vanishing {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] {f : α → G} (hf : Summable f) ⦃e : Set G⦄ (he : e ∈ nhds 0) : ∃ s, ∀ (t : Finset α), Disjoint t s → (Finset.sum t fun k => f k) ∈ e

theorem Summable.tendsto_cofinite_zero {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] {f : α → G} (hf : Summable f) : Filter.Tendsto f Filter.cofinite (nhds 0)

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

theorem Summable.tendsto_atTop_zero {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] {f : ℕ → G} (hf : Summable f) : Filter.Tendsto f Filter.atTop (nhds 0)

theorem Summable.countable_support {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] {f : α → G} [TopologicalSpace.FirstCountableTopology G] [T1Space G] (hf : Summable f) : Set.Countable (Function.support f)

theorem HasSum.const_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid γ] [TopologicalSpace α] [AddCommMonoid α] [DistribMulAction γ α] [ContinuousConstSMul γ α] {f : β → α} {a : α} (b : γ) (hf : HasSum f a) : HasSum (fun i => b • f i) (b • a)

theorem Summable.const_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid γ] [TopologicalSpace α] [AddCommMonoid α] [DistribMulAction γ α] [ContinuousConstSMul γ α] {f : β → α} (b : γ) (hf : Summable f) : Summable fun i => b • f i

theorem tsum_const_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid γ] [TopologicalSpace α] [AddCommMonoid α] [DistribMulAction γ α] [ContinuousConstSMul γ α] {f : β → α} [T2Space α] (b : γ) (hf : Summable f) : ∑' (i : β), b • f i = b • ∑' (i : β), f i

Infinite sums commute with scalar multiplication. Version for scalars living in a Monoid, but requiring a summability hypothesis.

theorem tsum_const_smul' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [AddCommMonoid α] {f : β → α} {γ : Type u_5} [Group γ] [DistribMulAction γ α] [ContinuousConstSMul γ α] [T2Space α] (g : γ) : ∑' (i : β), g • f i = g • ∑' (i : β), f i

Infinite sums commute with scalar multiplication. Version for scalars living in a Group, but not requiring any summability hypothesis.

theorem tsum_const_smul'' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [AddCommMonoid α] {f : β → α} {γ : Type u_5} [DivisionRing γ] [Module γ α] [ContinuousConstSMul γ α] [T2Space α] (g : γ) : ∑' (i : β), g • f i = g • ∑' (i : β), f i

Infinite sums commute with scalar multiplication. Version for scalars living in a DivisionRing; no summability hypothesis. This could be made to work for a [GroupWithZero γ] if there was such a thing as DistribMulActionWithZero.

Product and pi types

theorem HasSum.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [AddCommMonoid γ] [TopologicalSpace γ] {f : β → α} {g : β → γ} {a : α} {b : γ} (hf : HasSum f a) (hg : HasSum g b) : HasSum (fun x => (f x, g x)) (a, b)

theorem Pi.hasSum {α : Type u_1} {ι : Type u_5} {π : α → Type u_6} [(x : α) → AddCommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] {f : ι → (x : α) → π x} {g : (x : α) → π x} : HasSum f g ↔ ∀ (x : α), HasSum (fun i => f i x) (g x)

theorem Pi.summable {α : Type u_1} {ι : Type u_5} {π : α → Type u_6} [(x : α) → AddCommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] {f : ι → (x : α) → π x} : Summable f ↔ ∀ (x : α), Summable fun i => f i x

theorem tsum_apply {α : Type u_1} {ι : Type u_5} {π : α → Type u_6} [(x : α) → AddCommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] [∀ (x : α), T2Space (π x)] {f : ι → (x : α) → π x} {x : α} (hf : Summable f) : tsum ((x : α) → π x) Pi.addCommMonoid Pi.topologicalSpace ι (fun i => f i) x = ∑' (i : ι), f i x

Multiplicative opposite

theorem HasSum.op {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} (hf : HasSum f a) : HasSum (fun a => MulOpposite.op (f a)) (MulOpposite.op a)

theorem Summable.op {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (hf : Summable f) : Summable (MulOpposite.op ∘ f)

theorem HasSum.unop {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → αᵐᵒᵖ} {a : αᵐᵒᵖ} (hf : HasSum f a) : HasSum (fun a => MulOpposite.unop (f a)) (MulOpposite.unop a)

theorem Summable.unop {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → αᵐᵒᵖ} (hf : Summable f) : Summable (MulOpposite.unop ∘ f)

@[simp]

theorem hasSum_op {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} : HasSum (fun a => MulOpposite.op (f a)) (MulOpposite.op a) ↔ HasSum f a

@[simp]

theorem hasSum_unop {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → αᵐᵒᵖ} {a : αᵐᵒᵖ} : HasSum (fun a => MulOpposite.unop (f a)) (MulOpposite.unop a) ↔ HasSum f a

@[simp]

theorem summable_op {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} : (Summable fun a => MulOpposite.op (f a)) ↔ Summable f

@[simp]

theorem summable_unop {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → αᵐᵒᵖ} : (Summable fun a => MulOpposite.unop (f a)) ↔ Summable f

theorem tsum_op {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] : ∑' (x : β), MulOpposite.op (f x) = MulOpposite.op (∑' (x : β), f x)

theorem tsum_unop {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] {f : β → αᵐᵒᵖ} : ∑' (x : β), MulOpposite.unop (f x) = MulOpposite.unop (∑' (x : β), f x)

Interaction with the star

theorem HasSum.star {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : β → α} {a : α} (h : HasSum f a) : HasSum (fun b => star (f b)) (star a)

theorem Summable.star {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : β → α} (hf : Summable f) : Summable fun b => star (f b)

theorem Summable.ofStar {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : β → α} (hf : Summable fun b => star (f b)) : Summable f

@[simp]

theorem summable_star_iff {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : β → α} : (Summable fun b => star (f b)) ↔ Summable f

@[simp]

theorem summable_star_iff' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : β → α} : Summable (star f) ↔ Summable f

theorem tsum_star {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : β → α} [T2Space α] : star (∑' (b : β), f b) = ∑' (b : β), star (f b)

abbrev AddAction.automorphize.match_1 {α : Type u_2} {β : Type u_1} [AddGroup α] [AddAction α β] (b₁ : β) (b₂ : β) (motive : b₁ ≈ b₂ → Prop) : (h : b₁ ≈ b₂) → ((a : α) → (ha : a +ᵥ b₂ = b₁) → motive (_ : ∃ y, (fun m => m +ᵥ b₂) y = b₁)) → motive h

Equations

• AddAction.automorphize.match_1 b₁ b₂ motive h h_1 = Exists.casesOn h fun w h => h_1 w h

noncomputable def AddAction.automorphize {α : Type u_1} {β : Type u_2} {M : Type u_5} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] [AddGroup α] [AddAction α β] (f : β → M) : Quotient (AddAction.orbitRel α β) → M

Given an additive group α acting on a type β, and a function f : β → M, we automorphize f to a function β ⧸ α → M by summing over α orbits, b ↦ ∑' (a : α), f(a • b).

Equations

• AddAction.automorphize f = Quotient.lift (fun b => ∑' (a : α), f (a +ᵥ b)) (_ : ∀ (b₁ b₂ : β), b₁ ≈ b₂ → (fun b => ∑' (a : α), f (a +ᵥ b)) b₁ = (fun b => ∑' (a : α), f (a +ᵥ b)) b₂)

theorem AddAction.automorphize.proof_1 {α : Type u_2} {β : Type u_1} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] [AddGroup α] [AddAction α β] (f : β → M) (b₁ : β) (b₂ : β) : b₁ ≈ b₂ → (fun b => ∑' (a : α), f (a +ᵥ b)) b₁ = (fun b => ∑' (a : α), f (a +ᵥ b)) b₂

noncomputable def MulAction.automorphize {α : Type u_1} {β : Type u_2} {M : Type u_5} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] [Group α] [MulAction α β] (f : β → M) : Quotient (MulAction.orbitRel α β) → M

Given a group α acting on a type β, and a function f : β → M, we "automorphize" f to a function β ⧸ α → M by summing over α orbits, b ↦ ∑' (a : α), f(a • b).

Equations

• MulAction.automorphize f = Quotient.lift (fun b => ∑' (a : α), f (a • b)) (_ : ∀ (b₁ b₂ : β), b₁ ≈ b₂ → (fun b => ∑' (a : α), f (a • b)) b₁ = (fun b => ∑' (a : α), f (a • b)) b₂)

theorem MulAction.automorphize_smul_left {α : Type u_1} {β : Type u_2} {M : Type u_5} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] {R : Type u_6} [DivisionRing R] [Module R M] [ContinuousConstSMul R M] [Group α] [MulAction α β] (f : β → M) (g : Quotient (MulAction.orbitRel α β) → R) : MulAction.automorphize (g ∘ Quotient.mk' • f) = g • MulAction.automorphize f

Automorphization of a function into an R-module distributes, that is, commutes with the R-scalar multiplication.

theorem AddAction.automorphize_smul_left {α : Type u_1} {β : Type u_2} {M : Type u_5} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] {R : Type u_6} [DivisionRing R] [Module R M] [ContinuousConstSMul R M] [AddGroup α] [AddAction α β] (f : β → M) (g : Quotient (AddAction.orbitRel α β) → R) : AddAction.automorphize (g ∘ Quotient.mk' • f) = g • AddAction.automorphize f

Automorphization of a function into an R-module distributes, that is, commutes with the R-scalar multiplication.

noncomputable def QuotientAddGroup.automorphize {M : Type u_5} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] {G : Type u_7} [AddGroup G] {Γ : AddSubgroup G} (f : G → M) : G ⧸ Γ → M

Given a subgroup Γ of an additive group G, and a function f : G → M, we automorphize f to a function G ⧸ Γ → M by summing over Γ orbits, g ↦ ∑' (γ : Γ), f(γ • g).

Equations

• QuotientAddGroup.automorphize f = AddAction.automorphize f

noncomputable def QuotientGroup.automorphize {M : Type u_5} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] {G : Type u_7} [Group G] {Γ : Subgroup G} (f : G → M) : G ⧸ Γ → M

Given a subgroup Γ of a group G, and a function f : G → M, we "automorphize" f to a function G ⧸ Γ → M by summing over Γ orbits, g ↦ ∑' (γ : Γ), f(γ • g).

Equations

• QuotientGroup.automorphize f = MulAction.automorphize f

theorem QuotientGroup.automorphize_smul_left {M : Type u_5} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] {R : Type u_6} [DivisionRing R] [Module R M] [ContinuousConstSMul R M] {G : Type u_7} [Group G] {Γ : Subgroup G} (f : G → M) (g : G ⧸ Γ → R) : QuotientGroup.automorphize (g ∘ Quotient.mk' • f) = g • QuotientGroup.automorphize f

Automorphization of a function into an R-module distributes, that is, commutes with the R-scalar multiplication.

theorem QuotientAddGroup.automorphize_smul_left {M : Type u_5} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] {R : Type u_6} [DivisionRing R] [Module R M] [ContinuousConstSMul R M] {G : Type u_7} [AddGroup G] {Γ : AddSubgroup G} (f : G → M) (g : G ⧸ Γ → R) : QuotientAddGroup.automorphize (g ∘ Quotient.mk' • f) = g • QuotientAddGroup.automorphize f

Automorphization of a function into an R-module distributes, that is, commutes with the R-scalar multiplication.