Infinite sums in topological groups

Lemmas on topological sums in groups (as opposed to monoids).

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 : { x : β // x ∉ s }) => 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 : { x : β // x ∉ s }) => 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 : { x : β // x ∉ s }) => 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.

theorem summable_iff_cauchySeq_finset {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [CompleteSpace α] {f : β → α} : Summable f ↔ CauchySeq fun (s : Finset β) => 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 β) => Finset.sum s fun (b : β) => f b) ↔ ∀ e ∈ nhds 0, ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → (Finset.sum t fun (b : β) => f b) ∈ e

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

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

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

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 : Finset α), ∀ (t : Finset α), Disjoint t s → (Finset.sum t fun (k : α) => f k) ∈ e

theorem Summable.tsum_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 : Finset α), ∀ (t : Set α), Disjoint t ↑s → ∑' (b : ↑t), f ↑b ∈ e

theorem tendsto_tsum_compl_atTop_zero {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] (f : α → G) : Filter.Tendsto (fun (s : Finset α) => ∑' (a : { x : α // x ∉ s }), f ↑a) 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.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.countable_support {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] {f : α → G} [FirstCountableTopology G] [T1Space G] (hf : Summable f) : Set.Countable (Function.support f)

theorem summable_const_iff {β : Type u_2} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] [Infinite β] [T2Space G] (a : G) : (Summable fun (x : β) => a) ↔ a = 0

@[simp]

theorem tsum_const {β : Type u_2} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] [T2Space G] (a : G) : ∑' (x : β), a = Nat.card β • a