Research proof index

Evaluation of integral power series at a point of the open unit disc is multiplicative. Together with evalInt_add this makes evalInt q a ring homomorphism ℤ⟦X⟧ → k for each |q| < 1. Proof: on the open unit disc, evalInt is the coercion to k of mathlib's topological power-series evaluation over the ring of integers (key below): q is an inte...

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 convergence criterion for series over a nonarchimedean local field: if each term of f is bounded by |q|^(e i) for an exponent function e with finite sublevel sets, then f is summable , its terms tend to zero cofinitely, which suffices by completeness and the nonarchimedean property (no absolute convergence is needed , contrast the archimedean...

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...

The leading-term principle: if F = X + O(X²) then |F(q)| = |q| on the punctured open unit disc , ultrametrically the leading term dominates the tail, which has valuation at most |q|² by valuation_evalInt_le_pow.

If the first M coefficients of F vanish, its evaluation at a point of the open unit disc has valuation at most |q|^M: the partial sums satisfy the bound by the nonarchimedean triangle inequality, and it passes to the limit by the ultrametric isosceles principle (if v(σ - T) < v(T) and v(σ) < v(T) then v(T) ≤ max(v(σ), v(σ - T)) < v(T), absurd).