Norm estimates for null families in ultrametric groups

A family tending to zero along the cofinite filter is bounded. On a nonempty index type its largest norm is attained, including when every term has norm zero. This turns the non-strict ultrametric bound for infinite sums into two useful sharp statements.

For a family f with sum a in a seminormed ultrametric group, HasSum.norm_lt_of_forall_norm_lt shows that if every term has norm strictly less than a positive bound B, then ‖a‖ < B. The strict bound includes empty families and families whose terms all have norm zero. The result HasSum.norm_eq_of_forall_norm_lt says that if one term has norm strictly larger than every other term, then a has exactly the norm of that dominant term. Both estimates apply to every HasSum limit without completeness or Hausdorff assumptions.

Mathlib supplies the finite-sum estimate IsUltrametricDist.norm_sum_le_of_forall_le_of_nonneg and the term-removal identity hasSum_ite_sub_hasSum. The results here extend finite-sum bounds to strict bounds and dominant-term equalities for HasSum limits.

theorem Filter.Tendsto.exists_forall_norm_le {ι : Type u_1} {E : Type u_2} [SeminormedAddGroup E] [Nonempty ι] {f : ι → E} (hf : Tendsto f cofinite (nhds 0)) : ∃ (i : ι), ∀ (j : ι), ‖f j‖ ≤ ‖f i‖

A family on a nonempty index type tending to zero along the cofinite filter has a term whose norm dominates the norms of all its terms.

theorem Filter.Tendsto.exists_norm_eq_ciSup {ι : Type u_1} {E : Type u_2} [SeminormedAddGroup E] [Nonempty ι] {f : ι → E} (hf : Tendsto f cofinite (nhds 0)) : ∃ (i : ι), ‖f i‖ = ⨆ (j : ι), ‖f j‖

A family on a nonempty index type tending to zero along the cofinite filter attains the supremum of the norms of its terms.

theorem HasSum.norm_lt_of_forall_norm_lt {ι : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] [IsUltrametricDist E] {f : ι → E} {a : E} (hf : HasSum f a) {B : ℝ} (hB : 0 < B) (h : ∀ (i : ι), ‖f i‖ < B) : ‖a‖ < B

In an ultrametric group, any sum of a family whose terms all have norm strictly less than a positive bound B also has norm strictly less than B.

This includes empty families and families whose terms all have norm zero.

theorem HasSum.norm_eq_of_forall_norm_lt {ι : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] [IsUltrametricDist E] {f : ι → E} {a : E} (hf : HasSum f a) (i : ι) (hi : ∀ (j : ι), j ≠ i → ‖f j‖ < ‖f i‖) : ‖a‖ = ‖f i‖

In an ultrametric group, any sum of a family with a unique dominant term has the same norm as that term. Every other term must have strictly smaller norm than the distinguished term.