Infinite sums and products in nonarchimedean abelian groups

Let G be a complete nonarchimedean abelian group and let f : α → G be a function. We prove that f is unconditionally summable if and only if f a tends to zero on the cofinite filter on α. We also prove the analogous result in the multiplicative setting.

theorem NonarchimedeanAddGroup.cauchySeq_sum_of_tendsto_cofinite_zero {α : Type u_1} {G : Type u_2} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G] [NonarchimedeanAddGroup G] {f : α → G} (hf : Filter.Tendsto f Filter.cofinite (nhds 0)) : CauchySeq fun (s : Finset α) => Finset.sum s fun (i : α) => f i

Let G be a nonarchimedean additive abelian group, and let f : α → G be a function that tends to zero on the filter of cofinite sets. For each finite subset of α, consider the partial sum of f on that subset. These partial sums form a Cauchy filter.

theorem NonarchimedeanGroup.cauchySeq_prod_of_tendsto_cofinite_one {α : Type u_1} {G : Type u_2} [CommGroup G] [UniformSpace G] [UniformGroup G] [NonarchimedeanGroup G] {f : α → G} (hf : Filter.Tendsto f Filter.cofinite (nhds 1)) : CauchySeq fun (s : Finset α) => Finset.prod s fun (i : α) => f i

Let G be a nonarchimedean multiplicative abelian group, and let f : α → G be a function that tends to one on the filter of cofinite sets. For each finite subset of α, consider the partial product of f on that subset. These partial products form a Cauchy filter.

theorem NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero {α : Type u_1} {G : Type u_2} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G] [NonarchimedeanAddGroup G] [CompleteSpace G] {f : α → G} (hf : Filter.Tendsto f Filter.cofinite (nhds 0)) : Summable f

Let G be a complete nonarchimedean additive abelian group, and let f : α → G be a function that tends to zero on the filter of cofinite sets. Then f is unconditionally summable.

theorem NonarchimedeanGroup.multipliable_of_tendsto_cofinite_one {α : Type u_1} {G : Type u_2} [CommGroup G] [UniformSpace G] [UniformGroup G] [NonarchimedeanGroup G] [CompleteSpace G] {f : α → G} (hf : Filter.Tendsto f Filter.cofinite (nhds 1)) : Multipliable f

Let G be a complete nonarchimedean multiplicative abelian group, and let f : α → G be a function that tends to one on the filter of cofinite sets. Then f is unconditionally multipliable.

theorem NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero {α : Type u_1} {G : Type u_2} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G] [NonarchimedeanAddGroup G] [CompleteSpace G] (f : α → G) : Summable f ↔ Filter.Tendsto f Filter.cofinite (nhds 0)

Let G be a complete nonarchimedean additive abelian group. Then a function f : α → G is unconditionally summable if and only if it tends to zero on the filter of cofinite sets.

theorem NonarchimedeanGroup.multipliable_iff_tendsto_cofinite_one {α : Type u_1} {G : Type u_2} [CommGroup G] [UniformSpace G] [UniformGroup G] [NonarchimedeanGroup G] [CompleteSpace G] (f : α → G) : Multipliable f ↔ Filter.Tendsto f Filter.cofinite (nhds 1)

Let G be a complete nonarchimedean multiplicative abelian group. Then a function f : α → G is unconditionally multipliable if and only if it tends to one on the filter of cofinite sets.