Research proof index

Rearrangement for X (extracted from Silverman's proof of Advanced topics, Theorem V.3.1(c)): for 0 < ‖q‖ < ‖u‖ < 1 with u transcendental (so that evaluation of coefficients at u is a ring homomorphism), the coefficients of the formal series TateCurve.X evaluated at u sum to Xₐ(u, q). Proof: expand each term of Xₐ: for n ≥ 1, `qⁿu/(1 -...

Rearrangement for Y: for 0 < ‖q‖ < ‖u‖ < 1 with u transcendental, the coefficients of the formal series TateCurve.Y evaluated at u sum to Yₐ(u, q). Proof: as for hasSum_X_eval, using v²/(1-v)³ = ∑_{m ≥ 1} (m choose 2) vᵐ for the rows n ≥ 1, the rational-function identity v²/(1-v)³ = -v⁻¹/(1-v⁻¹)³ together with `v/(1-v)³ = ∑_{m ≥ 1} ((m...

The q-expansion of the Weierstrass ℘-function (Silverman, Advanced topics, Theorem I.6.2): for τ in the upper half plane and 0 < im z < im τ (which forces z ∉ Λ_τ), ℘(z; Λ_τ) = (2πi)² (1/12 + Xₐ(e z, e τ)). Proof: group the absolutely convergent sum defining ℘ into rows ω = nτ + m, n : ℤ (Fubini). The condition 0 < im z < im τ guaran...

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

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