Research proof index

Evaluation of integral power series commutes with valuative extensions of nonarchimedean local fields: the coefficients are (the same) integers on both sides, and both evaluations are within |q|^N of the common N-th partial sum (valuation_evalInt_sub_sum_le), whose bound transfers along the strictly monotone map of value groups , no continuity argum...

The geometric series over a nonarchimedean local field: for |x| < 1, x + x² + x³ + ⋯ = x/(1 - x). (Summability is by the nonarchimedean criterion , the terms tend to zero , and the value is identified through the partial sums x(xⁿ - 1)/(x - 1).)

The Lambert series rearrangement over a nonarchimedean local field: for any integer coefficients c and |q| < 1, ∑_{m≥1} c(m)qᵐ/(1 - qᵐ) = ∑_{N≥1} (∑_{d ∣ N} c(d))qᴺ. This is the valuative instantiation of the general tsum_lambert_of_summable (FLT.Slop.NumberTheory.TsumDivisorsAntidiagonal): the geometric row expansions come from `hasSum_geometri...

Quantitative tail bound: the evaluation of an integral power series on the open unit disc is within |q|^N of its N-th partial sum.