Valuation bounds on sums of series in a valuative topology #
Let R be a ring whose topology is induced by its valuative relation. For γ ≠ 0 the open ball
{z | v z < γ} is an open, hence closed, additive subgroup of R. So it contains the sum of any
series, convergent along any nontrivial summation filter, all of whose terms lie in it: this is
TauCeti.valuation_lt_of_hasSum.
theorem
TauCeti.valuation_lt_of_hasSum
{R : Type u_1}
[Ring R]
[ValuativeRel R]
[TopologicalSpace R]
[IsValuativeTopology R]
{ι : Type u_2}
{f : ι → R}
{s : R}
{L : SummationFilter ι}
[L.NeBot]
(hf : HasSum f s L)
(γ : (ValuativeRel.ValueGroupWithZero R)ˣ)
(h : ∀ (i : ι), (ValuativeRel.valuation R) (f i) < ↑γ)
:
If a series converges to s along a nontrivial summation filter and every term has valuation
less than the nonzero value γ, then s has valuation less than γ.