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 α (NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero). We also prove the analogous result in the multiplicative setting (NonarchimedeanGroup.multipliable_iff_tendsto_cofinite_one).

We also prove that multiplication distributes over arbitrarily indexed sums in a nonarchimedean ring. That is, let R be a nonarchimedean ring, let f : α → R be a function that sums to a : R, and let g : β → R be a function that sums to b : R. Then fun (i : α × β) ↦ (f i.1) * (g i.2) sums to a * b (HasSum.mul_of_nonarchimedean).

theorem NonarchimedeanGroup.cauchySeq_prod_of_tendsto_cofinite_one {α : Type u_1} {G : Type u_2} [CommGroup G] [UniformSpace G] [IsUniformGroup G] [NonarchimedeanGroup G] {f : α → G} (hf : Filter.Tendsto f Filter.cofinite (nhds 1)) : CauchySeq fun (s : Finset α) => ∏ i ∈ s, 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.cauchySeq_sum_of_tendsto_cofinite_zero {α : Type u_1} {G : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [NonarchimedeanAddGroup G] {f : α → G} (hf : Filter.Tendsto f Filter.cofinite (nhds 0)) : CauchySeq fun (s : Finset α) => ∑ i ∈ s, 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_of_tendsto_div_nhds_one {G : Type u_2} [CommGroup G] [UniformSpace G] [IsUniformGroup G] [NonarchimedeanGroup G] {f : ℕ → G} (hf : Filter.Tendsto (fun (n : ℕ) => f (n + 1) / f n) Filter.atTop (nhds 1)) : CauchySeq f

Let G be a nonarchimedean abelian group, and let f : ℕ → G be a function such that the quotients f (n + 1) / f n tend to one. Then the function is a Cauchy sequence.

theorem NonarchimedeanAddGroup.cauchySeq_of_tendsto_sub_nhds_zero {G : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [NonarchimedeanAddGroup G] {f : ℕ → G} (hf : Filter.Tendsto (fun (n : ℕ) => f (n + 1) - f n) Filter.atTop (nhds 0)) : CauchySeq f

Let G be a nonarchimedean additive abelian group, and let f : ℕ → G be a function such that the differences f (n + 1) - f n tend to zero. Then the function is a Cauchy sequence.

theorem NonarchimedeanGroup.multipliable_of_tendsto_cofinite_one {α : Type u_1} {G : Type u_2} [CommGroup G] [UniformSpace G] [IsUniformGroup 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_of_tendsto_cofinite_zero {α : Type u_1} {G : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup 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_iff_tendsto_cofinite_one {α : Type u_1} {G : Type u_2} [CommGroup G] [UniformSpace G] [IsUniformGroup 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.

theorem NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero {α : Type u_1} {G : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup 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 HasSum.mul_of_nonarchimedean {α : Type u_1} {β : Type u_2} {R : Type u_3} [Ring R] [UniformSpace R] [IsUniformAddGroup R] [NonarchimedeanRing R] {f : α → R} {g : β → R} {a b : R} (hf : HasSum f a) (hg : HasSum g b) : HasSum (fun (i : α × β) => f i.1 * g i.2) (a * b)

Let R be a nonarchimedean ring, let f : α → R be a function that sums to a : R, and let g : β → R be a function that sums to b : R. Then fun i : α × β ↦ f i.1 * g i.2 sums to a * b.

theorem Summable.mul_of_nonarchimedean {α : Type u_1} {β : Type u_2} {R : Type u_3} [Ring R] [UniformSpace R] [IsUniformAddGroup R] [NonarchimedeanRing R] {f : α → R} {g : β → R} (hf : Summable f) (hg : Summable g) : Summable fun (i : α × β) => f i.1 * g i.2

Let R be a nonarchimedean ring. If functions f : α → R and g : β → R are summable, then so is fun i : α × β ↦ f i.1 * g i.2.

theorem tsum_mul_tsum_of_nonarchimedean {α : Type u_1} {β : Type u_2} {R : Type u_3} [Ring R] [UniformSpace R] [IsUniformAddGroup R] [NonarchimedeanRing R] [T0Space R] {f : α → R} {g : β → R} (hf : Summable f) (hg : Summable g) : (∑' (i : α), f i) * ∑' (i : β), g i = ∑' (i : α × β), f i.1 * g i.2