Documentation

Mathlib.Topology.Algebra.InfiniteSum.Group

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) :
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) :
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) :
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 : α) :
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 : β // xs }) => 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 : β // xs }) => 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 : β // xs }) => 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) enhds 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) enhds 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 enhds 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 enhds 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) :
theorem Summable.indicator {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : βα} [CompleteSpace α] (hf : Summable f) (s : Set β) :
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) :
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 : β // xs }), 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 : α // xs }), 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_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