Documentation

Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

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 α) => is, 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 α) => is, 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.

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

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.

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.

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.