Bounded bilinear maps and infinite sums in ultrametric normed modules

A map bounded by a product of norms takes two cofinite-null families to a cofinite-null family on the product index. In a complete ultrametric target this gives summability; when the map is bilinear, passage to the completion gives double-sum and Cauchy-product identities without completeness. In the sum identities, the bilinear map is inferred from its norm bound. The scalar ring need not carry a norm, and neither source module needs to be complete or ultrametric. The double-sum argument follows HasSum.mul_eq in Mathlib.Topology.Algebra.InfiniteSum.Ring, with bounded bilinear maps in place of multiplication. Over an additive group index, such as the exponents of bilateral Laurent series, the fibres of addition are infinite; in a complete target they can still be summed, which gives the Cauchy product ∑' m, B (f m) (g (n - m)).

Under a bounded scalar action, the pointwise scalar multiples f i • g j of two cofinite-null families form a cofinite-null family on the product index. Consequently, over a complete ultrametric module this family is summable whenever f and g are, and so is the Cauchy product induced by the scalar action. If the action is moreover a module structure, then completeness is not needed: passing to the completion shows that the double sum of two families with sums a and b is a • b, and grouping it by the antidiagonals of an additive index type gives the corresponding Cauchy-product formula. The tsum forms of these identities assume the module is Hausdorff (stated as T0Space, which is equivalent for seminormed groups).

The joint-decay statement is stronger than continuity of scalar multiplication at zero: cofinite decay on a product index requires all but finitely many pairs to be small.

The summation API parallels Mathlib's nonarchimedean ring results HasSum.mul_of_nonarchimedean (whose passage to the completion we follow) and Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal, reusing the generic module and fiberwise-summation interfaces.

For bilateral Laurent series ∑ₙ f(n) uⁿ over a field, shifting the coefficients by k places multiplies the sum by uᵏ. The Cauchy product ∑' m, f(m) g(n - m) of the coefficients sums to the product of the two series over a complete normed field when both series converge absolutely, and over a complete ultrametric normed field whenever both series converge. In such a field the Cauchy product of two convergent bilateral series converges to the product of their sums, its moments ∑ n h(n) and ∑ (n (n - 1) / 2) h(n) obey the Leibniz rule, and multipliers of norm at most one preserve summability.

theorem TauCeti.tendsto_bilinear_cofinite_nhds_zero {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} {κ : Type u_6} [SeminormedAddGroup E] [SeminormedAddGroup F] [SeminormedAddGroup G] (B : E → F → G) {C : ℝ} (hB : ∀ (x : E) (y : F), ‖B x y‖ ≤ C * ‖x‖ * ‖y‖) {f : ι → E} {g : κ → F} (hf : Filter.Tendsto f Filter.cofinite (nhds 0)) (hg : Filter.Tendsto g Filter.cofinite (nhds 0)) : Filter.Tendsto (fun (ij : ι × κ) => B (f ij.1) (g ij.2)) Filter.cofinite (nhds 0)

A map bounded by a product of norms takes two cofinite-null families to a jointly cofinite-null family. No additivity or ultrametric hypothesis is needed.

theorem TauCeti.summable_bilinear_of_nonarchimedean {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} {κ : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [IsUltrametricDist G] [CompleteSpace G] (B : E → F → G) {C : ℝ} (hB : ∀ (x : E) (y : F), ‖B x y‖ ≤ C * ‖x‖ * ‖y‖) {f : ι → E} {g : κ → F} (hf : Summable f) (hg : Summable g) : Summable fun (ij : ι × κ) => B (f ij.1) (g ij.2)

Two summable families have a summable family of bilinear images in a complete ultrametric target. The norm bound, rather than additivity, gives summability.

theorem TauCeti.summable_sum_bilinear_antidiagonal_of_nonarchimedean {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [IsUltrametricDist G] (B : E → F → G) {C : ℝ} (hB : ∀ (x : E) (y : F), ‖B x y‖ ≤ C * ‖x‖ * ‖y‖) {A : Type u_7} [Add A] [Finset.HasAntidiagonal A] [CompleteSpace G] {f : A → E} {g : A → F} (hf : Summable f) (hg : Summable g) : Summable fun (n : A) => ∑ ij ∈ Finset.antidiagonal n, B (f ij.1) (g ij.2)

The antidiagonal Cauchy product is summable under a bilinear norm bound. Additivity of the map is not needed for this assertion.

theorem TauCeti.summable_sum_bilinear_range_of_nonarchimedean {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [IsUltrametricDist G] (B : E → F → G) {C : ℝ} (hB : ∀ (x : E) (y : F), ‖B x y‖ ≤ C * ‖x‖ * ‖y‖) [CompleteSpace G] {f : ℕ → E} {g : ℕ → F} (hf : Summable f) (hg : Summable g) : Summable fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), B (f k) (g (n - k))

The usual natural-number Cauchy product is summable under a bilinear norm bound.

theorem TauCeti.hasSum_bilinear_of_nonarchimedean {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} {κ : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [IsUltrametricDist G] [CommRing R] [Module R E] [Module R F] [Module R G] {B : E →ₗ[R] F →ₗ[R] G} {C : ℝ} (hB : ∀ (x : E) (y : F), ‖(B x) y‖ ≤ C * ‖x‖ * ‖y‖) {f : ι → E} {g : κ → F} {a : E} {b : F} (hf : HasSum f a) (hg : HasSum g b) : HasSum (fun (ij : ι × κ) => (B (f ij.1)) (g ij.2)) ((B a) b)

A bounded bilinear map commutes with two sums in an ultrametric target, with the sum taken over the product index.

theorem TauCeti.bilinear_tsum_tsum_of_nonarchimedean {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} {κ : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [IsUltrametricDist G] [CommRing R] [Module R E] [Module R F] [Module R G] {B : E →ₗ[R] F →ₗ[R] G} {C : ℝ} (hB : ∀ (x : E) (y : F), ‖(B x) y‖ ≤ C * ‖x‖ * ‖y‖) [T0Space G] {f : ι → E} {g : κ → F} (hf : Summable f) (hg : Summable g) : (B (∑' (i : ι), f i)) (∑' (j : κ), g j) = ∑' (ij : ι × κ), (B (f ij.1)) (g ij.2)

Evaluating a bounded bilinear map on two infinite sums equals its double sum.

theorem TauCeti.hasSum_sum_bilinear_antidiagonal_of_nonarchimedean {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [IsUltrametricDist G] [CommRing R] [Module R E] [Module R F] [Module R G] {B : E →ₗ[R] F →ₗ[R] G} {C : ℝ} (hB : ∀ (x : E) (y : F), ‖(B x) y‖ ≤ C * ‖x‖ * ‖y‖) {A : Type u_7} [Add A] [Finset.HasAntidiagonal A] {f : A → E} {g : A → F} {a : E} {b : F} (hf : HasSum f a) (hg : HasSum g b) : HasSum (fun (n : A) => ∑ ij ∈ Finset.antidiagonal n, (B (f ij.1)) (g ij.2)) ((B a) b)

Grouping a bilinear double sum by antidiagonals preserves its sum.

theorem TauCeti.bilinear_tsum_tsum_eq_tsum_sum_antidiagonal_of_nonarchimedean {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [IsUltrametricDist G] [CommRing R] [Module R E] [Module R F] [Module R G] {B : E →ₗ[R] F →ₗ[R] G} {C : ℝ} (hB : ∀ (x : E) (y : F), ‖(B x) y‖ ≤ C * ‖x‖ * ‖y‖) {A : Type u_7} [Add A] [Finset.HasAntidiagonal A] [T0Space G] {f : A → E} {g : A → F} (hf : Summable f) (hg : Summable g) : (B (∑' (n : A), f n)) (∑' (n : A), g n) = ∑' (n : A), ∑ ij ∈ Finset.antidiagonal n, (B (f ij.1)) (g ij.2)

The bilinear Cauchy-product formula for an additive index type.

theorem TauCeti.hasSum_tsum_bilinear_sub_of_nonarchimedean {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [IsUltrametricDist G] [CommRing R] [Module R E] [Module R F] [Module R G] {B : E →ₗ[R] F →ₗ[R] G} {C : ℝ} (hB : ∀ (x : E) (y : F), ‖(B x) y‖ ≤ C * ‖x‖ * ‖y‖) [CompleteSpace G] {A : Type u_7} [AddCommGroup A] {f : A → E} {g : A → F} {a : E} {b : F} (hf : HasSum f a) (hg : HasSum g b) : HasSum (fun (n : A) => ∑' (m : A), (B (f m)) (g (n - m))) ((B a) b)

The bilinear Cauchy product over an additive group index, such as the coefficients of a product of two bilateral Laurent series. The fibres of addition are infinite, so the target is assumed complete.

theorem TauCeti.hasSum_sum_bilinear_range_of_nonarchimedean {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [IsUltrametricDist G] [CommRing R] [Module R E] [Module R F] [Module R G] {B : E →ₗ[R] F →ₗ[R] G} {C : ℝ} (hB : ∀ (x : E) (y : F), ‖(B x) y‖ ≤ C * ‖x‖ * ‖y‖) {f : ℕ → E} {g : ℕ → F} {a : E} {b : F} (hf : HasSum f a) (hg : HasSum g b) : HasSum (fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), (B (f k)) (g (n - k))) ((B a) b)

The natural-number bilinear Cauchy product sums to the image of the two sums.

theorem TauCeti.bilinear_tsum_tsum_eq_tsum_sum_range_of_nonarchimedean {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [IsUltrametricDist G] [CommRing R] [Module R E] [Module R F] [Module R G] {B : E →ₗ[R] F →ₗ[R] G} {C : ℝ} (hB : ∀ (x : E) (y : F), ‖(B x) y‖ ≤ C * ‖x‖ * ‖y‖) [T0Space G] {f : ℕ → E} {g : ℕ → F} (hf : Summable f) (hg : Summable g) : (B (∑' (n : ℕ), f n)) (∑' (n : ℕ), g n) = ∑' (n : ℕ), ∑ k ∈ Finset.range (n + 1), (B (f k)) (g (n - k))

The natural-number bilinear Cauchy-product formula.

theorem Filter.Tendsto.smul_cofinite_nhds_zero {R : Type u_1} {M : Type u_2} [SeminormedAddGroup R] [SeminormedAddGroup M] [SMulZeroClass R M] [IsBoundedSMul R M] {α : Type u_3} {β : Type u_4} {f : α → R} {g : β → M} (hf : Tendsto f cofinite (nhds 0)) (hg : Tendsto g cofinite (nhds 0)) : Tendsto (fun (ij : α × β) => f ij.1 • g ij.2) cofinite (nhds 0)

If two normed families tend to zero cofinitely, then their pointwise scalar multiples, indexed by pairs, also tend to zero cofinitely.

theorem Summable.smul_of_nonarchimedean {R : Type u_1} {M : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] [SeminormedAddCommGroup R] [SMulZeroClass R M] [IsBoundedSMul R M] [CompleteSpace M] {α : Type u_3} {β : Type u_4} {f : α → R} {g : β → M} (hf : Summable f) (hg : Summable g) : Summable fun (ij : α × β) => f ij.1 • g ij.2

In a complete ultrametric normed group with a bounded scalar action, the pointwise scalar multiples of two summable families are summable on the product index.

theorem Summable.sum_smul_antidiagonal_of_nonarchimedean {R : Type u_1} {M : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] [SeminormedAddCommGroup R] [SMulZeroClass R M] [IsBoundedSMul R M] [CompleteSpace M] {A : Type u_3} [Add A] [Finset.HasAntidiagonal A] {f : A → R} {g : A → M} (hf : Summable f) (hg : Summable g) : Summable fun (n : A) => ∑ ij ∈ Finset.antidiagonal n, f ij.1 • g ij.2

In a complete ultrametric normed group with a bounded scalar action, the antidiagonal Cauchy product of two summable families is summable.

theorem Summable.sum_smul_range_of_nonarchimedean {R : Type u_1} {M : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] [SeminormedAddCommGroup R] [SMulZeroClass R M] [IsBoundedSMul R M] [CompleteSpace M] {f : ℕ → R} {g : ℕ → M} (hf : Summable f) (hg : Summable g) : Summable fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), f k • g (n - k)

In a complete ultrametric normed group with a bounded scalar action, the usual natural-number Cauchy product of two summable families is summable.

theorem HasSum.smul_of_nonarchimedean {R : Type u_1} {M : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] [SeminormedRing R] [Module R M] [IsBoundedSMul R M] {α : Type u_3} {β : Type u_4} {f : α → R} {g : β → M} {a : R} {b : M} (hf : HasSum f a) (hg : HasSum g b) : HasSum (fun (ij : α × β) => f ij.1 • g ij.2) (a • b)

Scalar multiplication distributes over two infinite sums in an ultrametric normed module.

theorem Summable.tsum_smul_tsum_of_nonarchimedean {R : Type u_1} {M : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] [SeminormedRing R] [Module R M] [IsBoundedSMul R M] [T0Space M] {α : Type u_3} {β : Type u_4} {f : α → R} {g : β → M} (hf : Summable f) (hg : Summable g) : (∑' (i : α), f i) • ∑' (j : β), g j = ∑' (ij : α × β), f ij.1 • g ij.2

The scalar multiple of two infinite sums in a Hausdorff ultrametric normed module is their double sum.

theorem HasSum.sum_smul_antidiagonal_of_nonarchimedean {R : Type u_1} {M : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] [SeminormedRing R] [Module R M] [IsBoundedSMul R M] {A : Type u_3} [Add A] [Finset.HasAntidiagonal A] {f : A → R} {g : A → M} {a : R} {b : M} (hf : HasSum f a) (hg : HasSum g b) : HasSum (fun (n : A) => ∑ ij ∈ Finset.antidiagonal n, f ij.1 • g ij.2) (a • b)

In an ultrametric normed module, the antidiagonal Cauchy product sums to the scalar multiple of the original two sums.

theorem Summable.tsum_smul_tsum_eq_tsum_sum_antidiagonal_of_nonarchimedean {R : Type u_1} {M : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] [SeminormedRing R] [Module R M] [IsBoundedSMul R M] {A : Type u_3} [Add A] [Finset.HasAntidiagonal A] [T0Space M] {f : A → R} {g : A → M} (hf : Summable f) (hg : Summable g) : (∑' (n : A), f n) • ∑' (n : A), g n = ∑' (n : A), ∑ ij ∈ Finset.antidiagonal n, f ij.1 • g ij.2

The Cauchy-product formula for the scalar multiple of two infinite sums, grouped over the antidiagonals of an additive index type, in a Hausdorff ultrametric normed module.

theorem Summable.tsum_smul_tsum_eq_tsum_sum_range_of_nonarchimedean {R : Type u_1} {M : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] [SeminormedRing R] [Module R M] [IsBoundedSMul R M] [T0Space M] {f : ℕ → R} {g : ℕ → M} (hf : Summable f) (hg : Summable g) : (∑' (n : ℕ), f n) • ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ Finset.range (n + 1), f k • g (n - k)

The natural-number Cauchy-product formula for the scalar multiple of two infinite sums, in a Hausdorff ultrametric normed module.

theorem HasSum.sum_smul_range_of_nonarchimedean {R : Type u_1} {M : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] [SeminormedRing R] [Module R M] [IsBoundedSMul R M] {f : ℕ → R} {g : ℕ → M} {a : R} {b : M} (hf : HasSum f a) (hg : HasSum g b) : HasSum (fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), f k • g (n - k)) (a • b)

In an ultrametric normed module, the natural-number Cauchy product sums to the scalar multiple of the original two sums.

Bilateral Laurent series

theorem TauCeti.hasSum_laurent_shift {K : Type u_3} [Field K] [TopologicalSpace K] [IsTopologicalSemiring K] {f : ℤ → K} {u : K} (hu : u ≠ 0) {s : K} (k : ℤ) (hf : HasSum (fun (n : ℤ) => f n * u ^ n) s) : HasSum (fun (n : ℤ) => f (n - k) * u ^ n) (u ^ k * s)

A Laurent series shifted by k places is multiplied by uᵏ.

theorem TauCeti.hasSum_laurent_mul_of_summable_norm {K : Type u_3} [NormedField K] [CompleteSpace K] {f g : ℤ → K} {u : K} (hu : u ≠ 0) (hf : Summable fun (n : ℤ) => ‖f n * u ^ n‖) (hg : Summable fun (n : ℤ) => ‖g n * u ^ n‖) : HasSum (fun (n : ℤ) => (∑' (m : ℤ), f m * g (n - m)) * u ^ n) ((∑' (n : ℤ), f n * u ^ n) * ∑' (n : ℤ), g n * u ^ n)

The Cauchy product of two absolutely convergent Laurent series over a complete normed field.

theorem TauCeti.hasSum_laurent_mul {K : Type u_3} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {f g : ℤ → K} {u : K} (hu : u ≠ 0) {a b : K} (hf : HasSum (fun (n : ℤ) => f n * u ^ n) a) (hg : HasSum (fun (n : ℤ) => g n * u ^ n) b) : HasSum (fun (n : ℤ) => (∑' (m : ℤ), f m * g (n - m)) * u ^ n) (a * b)

The Cauchy product of two convergent Laurent series.

theorem Summable.mul_sub {K : Type u_3} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {f g : ℤ → K} (hf : Summable f) (hg : Summable g) (n : ℤ) : Summable fun (m : ℤ) => f m * g (n - m)

Each coefficient ∑' m, f m * g (n - m) of the Cauchy product of two summable families is an unconditionally convergent sum.

theorem HasSum.tsum_mul_sub {K : Type u_3} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {f g : ℤ → K} {a b : K} (hf : HasSum f a) (hg : HasSum g b) : HasSum (fun (n : ℤ) => ∑' (m : ℤ), f m * g (n - m)) (a * b)

The Cauchy product of two convergent bilateral series over a complete ultrametric normed field: ∑ₙ ∑ₘ f(m) g(n - m) = (∑ f) (∑ g).

theorem HasSum.intCast_mul_tsum_mul_sub {K : Type u_3} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {f g : ℤ → K} {a a₁ b b₁ : K} (hf : HasSum f a) (hf₁ : HasSum (fun (n : ℤ) => ↑n * f n) a₁) (hg : HasSum g b) (hg₁ : HasSum (fun (n : ℤ) => ↑n * g n) b₁) : HasSum (fun (n : ℤ) => ↑n * ∑' (m : ℤ), f m * g (n - m)) (a₁ * b + a * b₁)

The Leibniz rule for first moments. The first moment ∑ n h(n) of the Cauchy product h = f * g is f₁ g₀ + f₀ g₁, where f₀ = ∑ f(n) and f₁ = ∑ n f(n).

theorem HasSum.intCast_mul_sub_one_ediv_two_mul_tsum_mul_sub {K : Type u_3} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {f g : ℤ → K} {a a₁ a₂ b b₁ b₂ : K} (hf : HasSum f a) (hf₁ : HasSum (fun (n : ℤ) => ↑n * f n) a₁) (hf₂ : HasSum (fun (n : ℤ) => ↑(n * (n - 1) / 2) * f n) a₂) (hg : HasSum g b) (hg₁ : HasSum (fun (n : ℤ) => ↑n * g n) b₁) (hg₂ : HasSum (fun (n : ℤ) => ↑(n * (n - 1) / 2) * g n) b₂) : HasSum (fun (n : ℤ) => ↑(n * (n - 1) / 2) * ∑' (m : ℤ), f m * g (n - m)) (a₂ * b + a₁ * b₁ + a * b₂)

The Leibniz rule for second moments. With the weights n (n - 1) / 2, the second moment of the Cauchy product h = f * g is f₂ g₀ + f₁ g₁ + f₀ g₂, where f₀ = ∑ f(n), f₁ = ∑ n f(n) and f₂ = ∑ (n (n - 1) / 2) f(n). The halved weights are integers, so this holds in every characteristic.

theorem TauCeti.summable_mul_of_norm_le_one {R : Type u_3} {ι : Type u_4} [SeminormedRing R] [IsUltrametricDist R] [CompleteSpace R] {f c : ι → R} (hf : Summable f) (hc : ∀ (i : ι), ‖c i‖ ≤ 1) : Summable fun (i : ι) => c i * f i

A family obtained from a summable one by multipliers of norm at most one is summable.