TateCurveConstruction.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

128 declarations, 0 contain sorry, 0 declared as axioms

The power series identity underlying the construction of the Tate curve

If k is a nonarchimedean local field and q ∈ kˣ has |q| < 1, then Tate showed that kˣ/qᶻ is the group of k-points of an elliptic curve E_q/k with Weierstrass equation y² + xy = x³ + a₄(q)x + a₆(q), for certain explicit power series a₄ and a₆ in q with integer coefficients; the map kˣ → E_q(k) is given by explicit power series X(u,q) and Y(u,q) in q whose coefficients are Laurent polynomials in u.

The purely algebraic input to this construction is the identity Y² + XY = X³ + a₄X + a₆ in ℚ(u)⟦q⟧, which this file states and proves (TateCurve.weierstrass_equation). The identity is extracted from Theorem V.1.1 of [Silverman, Advanced topics in the arithmetic of elliptic curves], where it is deduced from the complex-analytic theory of the Weierstrass ℘-function, using also its supporting results Theorem I.6.2 (the q-expansions of ℘ and ℘') and Theorem I.7.1 (the q-expansions of g₂ and g₃); see also the remark "In other words, we want to verify that this identity holds in the ring ℚ(u)[[q]]" in Silverman's proof of Theorem V.3.1(c).

Silverman's argument is complex-analytic, so an extra step (which Silverman leaves implicit) is needed to descend from an identity of convergent series of complex numbers to the identity of formal power series over ℚ(u): the coefficients of both sides are rational functions of u, and the analytic identity shows that they agree at infinitely many complex values of u, hence they agree in ℚ(u).

Strategy of the proof

Fix τ in the upper half plane and z ∈ ℂ, and set q = e(τ), u = e(z), where e(w) = exp(2πiw); let Λ_τ = ℤτ + ℤ (the PeriodPair.lattice of the pair (τ, 1)).

q-expansions (Silverman I.6.2, I.7.1). Prove
- ℘(z; Λ_τ) = (2πi)²(1/12 + Xₐ(u, q)) (weierstrassP_q_expansion),
- ℘'(z; Λ_τ) = (2πi)³(Xₐ(u, q) + 2Yₐ(u, q)) (derivWeierstrassP_q_expansion),
- g₂(Λ_τ) = (2πi)⁴(1 + 240s₃(q))/12 (g₂_q_expansion),
- g₃(Λ_τ) = -(2πi)⁶(1 - 504s₅(q))/216 (g₃_q_expansion),
where Xₐ, Yₐ, sₖ are the analytic functions defined below (sums over n : ℤ, resp. the convergent version of TateCurve.s). The main tool is the "row sum" identity ∑_{m : ℤ} (w + m)⁻ᵏ = ((-2πi)ᵏ/(k-1)!) ∑_{d ≥ 1} dᵏ⁻¹ e(w)ᵈ, obtained by differentiating the classical partial-fraction expansion of the cotangent; this is EisensteinSeries.qExpansion_identity in Mathlib (see also cot_series_rep and pi_mul_cot_pi_q_exp).
The analytic Weierstrass equation (Silverman V.1.1(a)). Substitute the expansions of step 1 into the differential equation ℘'² = 4℘³ - g₂℘ - g₃ (Mathlib's PeriodPair.derivWeierstrassP_sq) and simplify; after dividing by (2πi)⁶ and by 4, everything cancels to give analytic_weierstrass:
Yₐ² + XₐYₐ = Xₐ³ - 5s₃Xₐ - (5s₃ + 7s₅)/12.
Rearrangement. For 0 < ‖q‖ < ‖u‖ < 1, expand each term of the sums over n : ℤ defining Xₐ, Yₐ as a geometric-type series (v/(1-v)² = ∑ m vᵐ, v²/(1-v)³ = ∑ (m choose 2) vᵐ for ‖v‖ < 1), and rearrange the resulting absolutely convergent double series by powers of q. The coefficients that appear are exactly the coefficients of the formal series X and Y evaluated at u (hasSum_X_eval, hasSum_Y_eval; for transcendental u, so that evaluation of coefficients at u is a ring homomorphism).
Descent. If F ∈ ℚ(u)⟦q⟧ is such that, for infinitely many u₀ ∈ ℂ, the series ∑ₙ Fₙ(u₀)q₀ⁿ converges with sum 0 for all sufficiently small nonzero q₀, then F = 0 (eq_zero_of_forall_hasSum_zero): indeed each Fₙ(u₀) vanishes by uniqueness of coefficients of convergent power series, and a rational function with infinitely many zeros is zero. Applying this to F = Y² + XY - X³ - a₄X - a₆ with u₀ ranging over the (uncountably many, hence infinitely many) transcendental points of the punctured unit disc, steps 2 and 3 provide the vanishing hypothesis, and TateCurve.weierstrass_equation follows.

The supporting material lives in the namespace TateCurve.Blueprint.

Implementation notes

We work in (RatFunc ℚ)⟦X⟧, formal power series over the field ℚ(u) of rational functions. Beware of the clash of notation: the power series variable (written q above and in the references) is PowerSeries.X, whereas the rational function variable u is RatFunc.X, and neither has anything to do with the coordinate X on the curve, which is the power series TateCurve.X defined below.

There is also the possibility of a purely algebraic proof of the identity, avoiding complex analysis entirely; see https://mathoverflow.net/questions/469021/low-level-proof-of-identity-related-to-weierstrass-p-function This file does not take that route.

Other notes

Main statements written by Kevin Buzzard, slop proofs written by William Coram and Samual Yin, final clean-up done by codex, file now compiles in a couple of seconds.

Imports (11)

Imported by 1 file

FLT.lean

def TateCurve.s The power series sₖ = ∑_{n ≥ 1} σₖ(n)qⁿ ∈ ℚ(u)⟦q⟧ (where σₖ(n) is the sum of the kth powers of the positive divisors of n) line 136 source
Source documentation
The power series sₖ = ∑_{n ≥ 1} σₖ(n)qⁿ ∈ ℚ(u)⟦q⟧ (where σₖ(n) is the sum of the kth powers of the positive divisors of n). Up to a normalising constant, these are the q-expansions of the Eisenstein series of weight k + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, RatFunc, Rat
Proof uses: PowerSeries.mk, ArithmeticFunction, ArithmeticFunction.sigma
14 instances, coercions and auxiliary constants left out.
```
def s (k : ℕ) : (RatFunc ℚ)⟦X⟧ := .mk fun n ↦ (σ k n : RatFunc ℚ)
```
Mentions: TateCurve.X
def TateCurve.a₄ The coefficient a₄ = -5s₃ = -5q - 45q² - ⋯ of the Tate curve y² + xy = x³ + a₄x + a₆ line 140 source
Source documentation
The coefficient a₄ = -5s₃ = -5q - 45q² - ⋯ of the Tate curve y² + xy = x³ + a₄x + a₆.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, RatFunc, Rat
Proof uses: HMul.hMul, Unit, Neg.neg, OfNat.ofNat, TateCurve.s, Nat
23 instances, coercions and auxiliary constants left out.
```
def a₄ : (RatFunc ℚ)⟦X⟧ := -5 * s 3
```
Mentions: TateCurve.X, TateCurve.s
def TateCurve.a₆ The coefficient a₆ = -(5s₃ + 7s₅)/12 = -q - 23q² - ⋯ of the Tate curve y² + xy = x³ + a₄x + a₆ line 146 source
Source documentation
The coefficient a₆ = -(5s₃ + 7s₅)/12 = -q - 23q² - ⋯ of the Tate curve y² + xy = x³ + a₄x + a₆. (Division by 12 is implemented as scalar multiplication by 12⁻¹ ∈ ℚ(u); note that 5σ₃(n) + 7σ₅(n) is always divisible by 12, so a₆ in fact has integer coefficients, though we do not need this.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, RatFunc, Rat
Proof uses: HSMul.hSMul, Unit, Inv.inv, OfNat.ofNat, Neg.neg, HAdd.hAdd, HMul.hMul, TateCurve.s, Nat
36 instances, coercions and auxiliary constants left out.
```
def a₆ : (RatFunc ℚ)⟦X⟧ := (12 : RatFunc ℚ)⁻¹ • -(5 * s 3 + 7 * s 5)
```
Mentions: TateCurve.X, TateCurve.s
def TateCurve.X The power series X(u,q) = u/(1-u)² + ∑_{n ≥ 1} (∑_{d ∣ n} d(uᵈ + u⁻ᵈ - 2)) qⁿ ∈ ℚ(u)⟦q⟧, the x-coordinate of the uniformisation kˣ/qᶻ ≃ E_q(k) of the Tate curve line 151 source
Source documentation
The power series X(u,q) = u/(1-u)² + ∑_{n ≥ 1} (∑_{d ∣ n} d(uᵈ + u⁻ᵈ - 2)) qⁿ ∈ ℚ(u)⟦q⟧, the x-coordinate of the uniformisation kˣ/qᶻ ≃ E_q(k) of the Tate curve.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, RatFunc, Rat
Proof uses: HAdd.hAdd, Unit, RingHom, PowerSeries.C, HDiv.hDiv, RatFunc.X, HPow.hPow, Nat, HSub.hSub, OfNat.ofNat, PowerSeries.mk, Finset.sum, Nat.divisors, HMul.hMul, Inv.inv
38 instances, coercions and auxiliary constants left out.
```
def X : (RatFunc ℚ)⟦X⟧ :=
…
```
def TateCurve.Y Documented declaration: Y line 158 source
Source documentation
The power series Y(u,q) = u²/(1-u)³ + ∑_{n ≥ 1} (∑_{d ∣ n} ((d choose 2)uᵈ - (d+1 choose 2)u⁻ᵈ + d)) qⁿ in ℚ(u)⟦q⟧, the y-coordinate of the uniformisation kˣ/qᶻ ≃ E_q(k) of the Tate curve.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, RatFunc, Rat
Proof uses: HAdd.hAdd, Unit, RingHom, PowerSeries.C, HDiv.hDiv, HPow.hPow, Nat, RatFunc.X, OfNat.ofNat, HSub.hSub, PowerSeries.mk, Finset.sum, Nat.divisors, HMul.hMul, Nat.choose, Inv.inv
37 instances, coercions and auxiliary constants left out.
```
def Y : (RatFunc ℚ)⟦X⟧ := .C (u ^ 2 / (1 - u) ^ 3) + .mk fun n ↦ ∑ d ∈ n.divisors,
…
```
Mentions: TateCurve.X
def TateCurve.Blueprint.e e z = exp (2πiz) line 168 source
Source documentation
e z = exp (2πiz). We will take u = e z and q = e τ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex
Proof uses: Complex.exp, HMul.hMul, OfNat.ofNat, Real.pi, Complex.I
6 instances, coercions and auxiliary constants left out.
```
def e (z : ℂ) : ℂ := Complex.exp (2 * (Real.pi : ℂ) * I * z)
```
lemma TateCurve.Blueprint.e_ne_zero line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Ne, TateCurve.Blueprint.e, OfNat.ofNat
Proof uses: Complex.exp_ne_zero, HMul.hMul, Real.pi, Complex.I
8 instances, coercions and auxiliary constants left out.
lemma TateCurve.Blueprint.e_add line 172 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, TateCurve.Blueprint.e, HAdd.hAdd, HMul.hMul
Proof uses: Eq.mpr, Complex.exp, OfNat.ofNat, Real.pi, Complex.I, id, congrArg, of_eq_true, Eq.trans, Nat, True, congr, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.atom_pf and 22 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TateCurve.Blueprint.e_neg line 176 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, TateCurve.Blueprint.e, Neg.neg, Inv.inv
Proof uses: Eq.mpr, Complex.exp, HMul.hMul, OfNat.ofNat, Real.pi, Complex.I, id, congrArg, of_eq_true, Eq.trans, Nat, True, congr, HAdd.hAdd, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 37 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TateCurve.Blueprint.e_intMul line 180 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Complex, Eq, TateCurve.Blueprint.e, HMul.hMul, HPow.hPow
Proof uses: Eq.mpr, Complex.exp, OfNat.ofNat, Real.pi, Complex.I, id, congrArg, of_eq_true, Eq.trans, Nat, True, congr, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.atom_pf and 18 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TateCurve.Blueprint.e_sub_intCast_mul line 184 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Int, Eq, TateCurve.Blueprint.e, HSub.hSub, HMul.hMul, HPow.hPow, Neg.neg
Proof uses: Eq.mpr, HAdd.hAdd, id, congrArg, sub_eq_add_neg, TateCurve.Blueprint.e_add, mul_comm, Eq.symm, neg_mul, Int.cast_neg, TateCurve.Blueprint.e_intMul, Eq.refl
47 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma TateCurve.Blueprint.e_intCast_mul_natAbs line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LE.le, OfNat.ofNat, Complex, Eq, TateCurve.Blueprint.e, HMul.hMul, HPow.hPow, Nat, Int.natAbs
Proof uses: Eq.mpr, id, congrArg, Eq.symm, Int.natAbs_of_nonneg, TateCurve.Blueprint.e_intMul, zpow_natCast, Eq.refl
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma TateCurve.Blueprint.e_neg_intCast_mul_natAbs line 191 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LE.le, OfNat.ofNat, Complex, Eq, TateCurve.Blueprint.e, Neg.neg, HMul.hMul, HPow.hPow, Nat, Int.natAbs
Proof uses: Eq.mpr, id, congrArg, Eq.symm, neg_mul, Int.cast_neg, Int.ofNat_natAbs_of_nonpos, TateCurve.Blueprint.e_intMul, zpow_natCast, Eq.refl
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma TateCurve.Blueprint.norm_e line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, Real, Norm.norm, TateCurve.Blueprint.e, Real.exp, Neg.neg, HMul.hMul, OfNat.ofNat, Nat, Real.pi, Complex.im
Proof uses: Eq.mpr, HSub.hSub, HAdd.hAdd, Complex.re, id, congrFun', congrArg, Eq.trans, Complex.exp, Complex.I, Complex.norm_exp, Complex.mul_re, congr, Complex.mul_im, of_eq_true, True, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance and 43 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TateCurve.Blueprint.norm_e_lt_one line 200 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LT.lt, Real, OfNat.ofNat, Complex.im, Norm.norm, TateCurve.Blueprint.e
Proof uses: of_eq_true, Eq.trans, Neg.neg, HMul.hMul, Nat, Real.pi, True, Real.exp, congrFun', congrArg, TateCurve.Blueprint.norm_e, eq_true
62 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma TateCurve.Blueprint.norm_e_lt_norm_e line 203 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LT.lt, Real, Complex.im, Norm.norm, TateCurve.Blueprint.e
Proof uses: of_eq_true, Eq.trans, Neg.neg, HMul.hMul, OfNat.ofNat, Nat, Real.pi, True, Real.exp, congr, congrArg, TateCurve.Blueprint.norm_e, HAdd.hAdd, eq_true
68 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma TateCurve.Blueprint.two_pi_I_ne_zero line 206 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ne, Complex, HMul.hMul, OfNat.ofNat, Nat, Real.pi, Complex.I
Proof uses: of_eq_true, Not, Eq, Eq.trans, False, True, congrArg, Or, congr, Real, or_self, not_false_eq_true
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def TateCurve.Blueprint.periodPair The pair of periods (τ, 1), for τ not real line 210 source
Source documentation
The pair of periods (τ, 1), for τ not real. Its PeriodPair.lattice is Λ_τ = ℤτ + ℤ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Ne, Real, Complex.im, OfNat.ofNat, PeriodPair
Proof uses: PeriodPair.mk
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def periodPair (τ : ℂ) (hτ : τ.im ≠ 0) : PeriodPair where
…
```
lemma TateCurve.Blueprint.periodPair_ω₁ line 217 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Ne, Real, Complex.im, OfNat.ofNat, Eq, PeriodPair.ω₁, TateCurve.Blueprint.periodPair
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma TateCurve.Blueprint.periodPair_ω₂ line 219 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Ne, Real, Complex.im, OfNat.ofNat, Eq, PeriodPair.ω₂, TateCurve.Blueprint.periodPair
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma TateCurve.Blueprint.hasSum_lattice_prod Transport of a HasSum over the lattice Λ_τ = ℤτ + ℤ along the reindexing ℤ × ℤ ≃ Λ_τ, (n, m) ↦ nτ + m line 223 source
Source documentation
Transport of a HasSum over the lattice Λ_τ = ℤτ + ℤ along the reindexing ℤ × ℤ ≃ Λ_τ, (n, m) ↦ nτ + m.
```
private lemma hasSum_lattice_prod {τ : ℂ} (hτ : τ.im ≠ 0) {f : ℂ → ℂ} {S : ℂ}
    (h : HasSum (fun l : (periodPair τ hτ).lattice ↦ f l) S) :
    HasSum (fun p : ℤ × ℤ ↦ f (p.1 * τ + p.2)) S := by
…
```
Mentions: TateCurve.Blueprint.periodPair
def TateCurve.Blueprint.sAn The convergent power series sₖ(q) = ∑_{n ≥ 1} σₖ(n)qⁿ, for ‖q‖ < 1 (junk value otherwise); the evaluation of the formal series TateCurve.s k at q line 232 source
Source documentation
The convergent power series sₖ(q) = ∑_{n ≥ 1} σₖ(n)qⁿ, for ‖q‖ < 1 (junk value otherwise); the evaluation of the formal series TateCurve.s k at q. Convergence follows from the crude estimate σₖ(n) ≤ n^(k+1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex
Proof uses: tsum, HMul.hMul, ArithmeticFunction, ArithmeticFunction.sigma, HPow.hPow, SummationFilter.unconditional
21 instances, coercions and auxiliary constants left out.
```
def sAn (k : ℕ) (q : ℂ) : ℂ := ∑' n : ℕ, (σ k n : ℂ) * q ^ n
```
def TateCurve.Blueprint.XAn The analytic function Xₐ(u, q) = ∑_{n : ℤ} qⁿu/(1 - qⁿu)² - 2s₁(q), defined for 0 < ‖q‖ < 1 and u ∉ qᶻ (junk value otherwise) line 239 source
Source documentation
The analytic function Xₐ(u, q) = ∑_{n : ℤ} qⁿu/(1 - qⁿu)² - 2s₁(q), defined for 0 < ‖q‖ < 1 and u ∉ qᶻ (junk value otherwise). This is the function called X(u, q) in [Silverman, Advanced topics, Theorem V.1.1]. The sum converges absolutely: the terms for n → ∞ are O(‖q‖ⁿ), and likewise for n → -∞ after rewriting v/(1-v)² = v⁻¹/(1-v⁻¹)² with v = qⁿu.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex
Proof uses: HSub.hSub, tsum, Int, HDiv.hDiv, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, SummationFilter.unconditional, TateCurve.Blueprint.sAn
28 instances, coercions and auxiliary constants left out.
```
def XAn (u q : ℂ) : ℂ := (∑' n : ℤ, q ^ n * u / (1 - q ^ n * u) ^ 2) - 2 * sAn 1 q
```
Mentions: TateCurve.Blueprint.sAn
def TateCurve.Blueprint.YAn The analytic function Yₐ(u, q) = ∑_{n : ℤ} (qⁿu)²/(1 - qⁿu)³ + s₁(q), defined for 0 < ‖q‖ < 1 and u ∉ qᶻ (junk value otherwise) line 244 source
Source documentation
The analytic function Yₐ(u, q) = ∑_{n : ℤ} (qⁿu)²/(1 - qⁿu)³ + s₁(q), defined for 0 < ‖q‖ < 1 and u ∉ qᶻ (junk value otherwise). This is the function called Y(u, q) in [Silverman, Advanced topics, Theorem V.1.1].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex
Proof uses: HAdd.hAdd, tsum, Int, HDiv.hDiv, HPow.hPow, Nat, HMul.hMul, OfNat.ofNat, HSub.hSub, SummationFilter.unconditional, TateCurve.Blueprint.sAn
27 instances, coercions and auxiliary constants left out.
```
def YAn (u q : ℂ) : ℂ := (∑' n : ℤ, (q ^ n * u) ^ 2 / (1 - q ^ n * u) ^ 3) + sAn 1 q
```
Mentions: TateCurve.Blueprint.sAn
lemma TateCurve.Blueprint.hasSum_choose_two_mul_geometric The Lambert-type sum ∑_{n ≥ 0} (n choose 2)rⁿ = r²/(1 - r)³ for ‖r‖ < 1, by shifting the index in ∑' n, ((n + 2).choose 2) * rⁿ = 1/(1 - r)³ line 258 source
Source documentation
The Lambert-type sum ∑_{n ≥ 0} (n choose 2)rⁿ = r²/(1 - r)³ for ‖r‖ < 1, by shifting the index in ∑' n, ((n + 2).choose 2) * rⁿ = 1/(1 - r)³.
```
private lemma hasSum_choose_two_mul_geometric {r : ℂ} (hr : ‖r‖ < 1) :
    HasSum (fun n : ℕ ↦ ((n.choose 2 : ℕ) : ℂ) * r ^ n) (r ^ 2 * ((1 - r) ^ 3)⁻¹) := by
…
```
lemma TateCurve.Blueprint.tsum_sq_mul_geometric_of_norm_lt_one Documented declaration: tsum_sq_mul_geometric_of_norm_lt_one line 271 source
Source documentation
The Lambert-type sum ∑_{n ≥ 0} n²rⁿ = r(1 + r)/(1 - r)³ for ‖r‖ < 1, from the n(n-1)/2- and n-sums (hasSum_choose_two_mul_geometric, hasSum_coe_mul_geometric_of_norm_lt_one).
```
private lemma tsum_sq_mul_geometric_of_norm_lt_one {r : ℂ} (hr : ‖r‖ < 1) :
    ∑' n : ℕ, (n : ℂ) ^ 2 * r ^ n = r * (1 + r) / (1 - r) ^ 3 := by
…
```
lemma TateCurve.Blueprint.sum_int_inv_pow_succ Row sum, exponent k + 1 ≥ 2, with the Lambert sum in series form: for w in the upper half plane, ∑_{m : ℤ} (w + m)⁻⁽ᵏ⁺¹⁾ = ((-2πi)ᵏ⁺¹/k!) ∑_{d ≥ 0} dᵏ e(w)ᵈ line 293 source
Source documentation
Row sum, exponent k + 1 ≥ 2, with the Lambert sum in series form: for w in the upper half plane, ∑_{m : ℤ} (w + m)⁻⁽ᵏ⁺¹⁾ = ((-2πi)ᵏ⁺¹/k!) ∑_{d ≥ 0} dᵏ e(w)ᵈ. This is EisensteinSeries.qExpansion_identity.
```
private lemma sum_int_inv_pow_succ (w : ℂ) (hw : 0 < w.im) {k : ℕ} (hk : 1 ≤ k) :
    ∑' m : ℤ, ((w + m) ^ (k + 1))⁻¹
      = (-2 * (Real.pi : ℂ) * I) ^ (k + 1) / (k.factorial : ℂ)
        * ∑' d : ℕ, (d : ℂ) ^ k * e w ^ d := by
…
```
Mentions: TateCurve.Blueprint.e
theorem TateCurve.Blueprint.sum_int_inv_sq Row sum, exponent 2: for w in the upper half plane, ∑_{m : ℤ} (w + m)⁻² = (2πi)² e(w)/(1 - e(w))² line 303 source
Source documentation
Row sum, exponent 2: for w in the upper half plane, ∑_{m : ℤ} (w + m)⁻² = (2πi)² e(w)/(1 - e(w))². This is the case k = 1 of sum_int_inv_pow_succ together with the closed form of the Lambert sum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LT.lt, Real, OfNat.ofNat, Complex.im, Eq, tsum, Int, Inv.inv, HPow.hPow, Nat, HAdd.hAdd, SummationFilter.unconditional, HMul.hMul, Real.pi, Complex.I, HDiv.hDiv, TateCurve.Blueprint.e, HSub.hSub
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Neg.neg, Nat.factorial, le_rfl, congr, neg_mul, Even.neg_pow, Even, Nat.cast_one, div_one, SummationFilter, optParam, funext, pow_one, tsum_coe_mul_geometric_of_norm_lt_one, TateCurve.Blueprint.norm_e_lt_one and 1 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem sum_int_inv_sq (w : ℂ) (hw : 0 < w.im) :
    ∑' m : ℤ, ((w + m) ^ 2)⁻¹ = (2 * (Real.pi : ℂ) * I) ^ 2 * (e w / (1 - e w) ^ 2) := by
…
```
Mentions: TateCurve.Blueprint.e
theorem TateCurve.Blueprint.sum_int_inv_cube Documented declaration: sum_int_inv_cube line 312 source
Source documentation
Row sum, exponent 3: for w in the upper half plane, ∑_{m : ℤ} (w + m)⁻³ = -(2πi)³/2 ⬝ e(w)(1 + e(w))/(1 - e(w))³ (note the sign: the exponent is odd, and the general formula has (-2πi)ᵏ/(k-1)!). This is the case k = 2 of sum_int_inv_pow_succ together with the closed form of the Lambert sum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LT.lt, Real, OfNat.ofNat, Complex.im, Eq, tsum, Int, Inv.inv, HPow.hPow, Nat, HAdd.hAdd, SummationFilter.unconditional, HMul.hMul, HDiv.hDiv, Neg.neg, Real.pi, Complex.I, TateCurve.Blueprint.e, HSub.hSub
Proof uses: Nat.factorial, one_le_two, Eq.mpr, id, congrArg, TateCurve.Blueprint.norm_e_lt_one, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.div_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo and 67 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem sum_int_inv_cube (w : ℂ) (hw : 0 < w.im) :
    ∑' m : ℤ, ((w + m) ^ 3)⁻¹ =
      -(2 * (Real.pi : ℂ) * I) ^ 3 / 2 * (e w * (1 + e w) / (1 - e w) ^ 3) := by
…
```
Mentions: TateCurve.Blueprint.e
lemma TateCurve.Blueprint.summable_int_inv_pow ∑_{m : ℤ} (w + m)⁻ᵏ converges (absolutely) for every w and k ≥ 2 line 321 source
Source documentation
∑_{m : ℤ} (w + m)⁻ᵏ converges (absolutely) for every w and k ≥ 2.
```
private lemma summable_int_inv_pow (w : ℂ) {k : ℕ} (hk : 2 ≤ k) :
    Summable fun m : ℤ ↦ ((w + m) ^ k)⁻¹ :=
…
```
lemma TateCurve.Blueprint.summable_comp_neg line 326 source
lemma TateCurve.Blueprint.summable_int_inv_pow_sub line 330 source
lemma TateCurve.Blueprint.tsum_int_inv_pow_sub line 334 source
lemma TateCurve.Blueprint.tsum_int_inv_pow_neg Evenness of the row sum under w ↦ -w, for even exponents line 340 source
Source documentation
Evenness of the row sum under w ↦ -w, for even exponents.
```
private lemma tsum_int_inv_pow_neg (w : ℂ) {k : ℕ} (hk : Even k) :
    ∑' m : ℤ, ((w + m) ^ k)⁻¹ = ∑' m : ℤ, ((-w + m) ^ k)⁻¹ := by
…
```
lemma TateCurve.Blueprint.tsum_int_inv_pow_neg_odd Oddness of the row sum under w ↦ -w, for odd exponents line 348 source
Source documentation
Oddness of the row sum under w ↦ -w, for odd exponents.
```
private lemma tsum_int_inv_pow_neg_odd (w : ℂ) {k : ℕ} (hk : Odd k) :
    ∑' m : ℤ, ((w + m) ^ k)⁻¹ = -∑' m : ℤ, ((-w + m) ^ k)⁻¹ := by
…
```
lemma TateCurve.Blueprint.hasSum_int_inv_pow The Basel-type sums over ℤ: ∑_{m : ℤ} m⁻ᵏ = 2ζ(k) for even k ≥ 2 (the m = 0 term is junk 0) line 357 source
Source documentation
The Basel-type sums over ℤ: ∑_{m : ℤ} m⁻ᵏ = 2ζ(k) for even k ≥ 2 (the m = 0 term is junk 0).
```
private lemma hasSum_int_inv_pow {k : ℕ} (hk : 2 ≤ k) (hk2 : Even k) :
    HasSum (fun m : ℤ ↦ ((m : ℂ) ^ k)⁻¹) (2 * riemannZeta k) := by
…
```
lemma TateCurve.Blueprint.one_sub_inv_ne_zero line 362 source
lemma TateCurve.Blueprint.inv_div_one_sub_inv_sq The rational-function identity v⁻¹/(1 - v⁻¹)² = v/(1 - v)² (true for v ≠ 0, including v = 1 where both sides are junk 0) line 367 source
Source documentation
The rational-function identity v⁻¹/(1 - v⁻¹)² = v/(1 - v)² (true for v ≠ 0, including v = 1 where both sides are junk 0).
```
private lemma inv_div_one_sub_inv_sq {v : ℂ} (hv : v ≠ 0) :
    v⁻¹ / (1 - v⁻¹) ^ 2 = v / (1 - v) ^ 2 := by
…
```
lemma TateCurve.Blueprint.norm_pow_div_one_sub_pow_le Norm bound for vʲ/(1 - v)ᵏ when ‖v‖ ≤ a < 1 line 375 source
Source documentation
Norm bound for vʲ/(1 - v)ᵏ when ‖v‖ ≤ a < 1.
```
private lemma norm_pow_div_one_sub_pow_le {v : ℂ} {a : ℝ} (hva : ‖v‖ ≤ a) (ha : a < 1)
    (j k : ℕ) : ‖v ^ j / (1 - v) ^ k‖ ≤ ‖v‖ ^ j / (1 - a) ^ k := by
…
```
lemma TateCurve.Blueprint.summable_aux' If ‖x‖ < 1 and ‖xy‖ < 1 then ∑_{n ≥ 1} (xⁿy)ʲ/(1 - xⁿy)ᵏ converges for j ≥ 1 (the terms decay geometrically) line 389 source
Source documentation
If ‖x‖ < 1 and ‖xy‖ < 1 then ∑_{n ≥ 1} (xⁿy)ʲ/(1 - xⁿy)ᵏ converges for j ≥ 1 (the terms decay geometrically).
```
private lemma summable_aux' {x y : ℂ} (hx : ‖x‖ < 1) (hxy : ‖x * y‖ < 1) {j k : ℕ}
    (hj : 1 ≤ j) :
    Summable fun n : ℕ ↦ (x ^ (n + 1) * y) ^ j / (1 - x ^ (n + 1) * y) ^ k := by
…
```
lemma TateCurve.Blueprint.summable_aux If ‖x‖ < 1 and ‖xy‖ < 1 then ∑_{n ≥ 1} xⁿy/(1 - xⁿy)² converges (the terms decay geometrically) line 405 source
Source documentation
If ‖x‖ < 1 and ‖xy‖ < 1 then ∑_{n ≥ 1} xⁿy/(1 - xⁿy)² converges (the terms decay geometrically).
```
private lemma summable_aux {x y : ℂ} (hx : ‖x‖ < 1) (hxy : ‖x * y‖ < 1) :
    Summable fun n : ℕ ↦ x ^ (n + 1) * y / (1 - x ^ (n + 1) * y) ^ 2 :=
…
```
lemma TateCurve.Blueprint.sum_int_inv_sq' Extension of sum_int_inv_sq to w in the lower half plane, using the evenness of w ↦ ∑_m (w + m)⁻² and the invariance of v/(1-v)² under v ↦ v⁻¹ line 411 source
Source documentation
Extension of sum_int_inv_sq to w in the lower half plane, using the evenness of w ↦ ∑_m (w + m)⁻² and the invariance of v/(1-v)² under v ↦ v⁻¹.
```
private lemma sum_int_inv_sq' (w : ℂ) (hw : w.im ≠ 0) :
    ∑' m : ℤ, ((w + m) ^ 2)⁻¹ = (2 * (Real.pi : ℂ) * I) ^ 2 * (e w / (1 - e w) ^ 2) := by
…
```
Mentions: TateCurve.Blueprint.e
lemma TateCurve.Blueprint.hasSum_int_inv_sq The Basel problem over ℤ: ∑_{m : ℤ} m⁻² = π²/3 (the m = 0 term is junk 0) line 419 source
Source documentation
The Basel problem over ℤ: ∑_{m : ℤ} m⁻² = π²/3 (the m = 0 term is junk 0).
```
private lemma hasSum_int_inv_sq :
    HasSum (fun m : ℤ ↦ ((m : ℂ) ^ 2)⁻¹) ((Real.pi : ℂ) ^ 2 / 3) := by
…
```
lemma TateCurve.Blueprint.tsum_pnat_of_zero Dropping a vanishing 0th term: ∑'_{n : ℕ+} g n = ∑'_{n : ℕ} g n when g 0 = 0 (true without summability hypotheses, since both sides are junk simultaneously) line 427 source
Source documentation
Dropping a vanishing 0th term: ∑'_{n : ℕ+} g n = ∑'_{n : ℕ} g n when g 0 = 0 (true without summability hypotheses, since both sides are junk simultaneously).
```
private lemma tsum_pnat_of_zero (g : ℕ → ℂ) (hg0 : g 0 = 0) :
    ∑' n : ℕ+, g n = ∑' n : ℕ, g n := by
…
```
lemma TateCurve.Blueprint.tsum_pnat_coe_mul_geometric The Lambert sum over ℕ+: ∑_{c ≥ 1} c xᶜ = x/(1 - x)² for ‖x‖ < 1 line 436 source
Source documentation
The Lambert sum over ℕ+: ∑_{c ≥ 1} c xᶜ = x/(1 - x)² for ‖x‖ < 1.
```
private lemma tsum_pnat_coe_mul_geometric {x : ℂ} (hx : ‖x‖ < 1) :
    ∑' c : ℕ+, (c : ℂ) * x ^ (c : ℕ) = x / (1 - x) ^ 2 := by
…
```
lemma TateCurve.Blueprint.summable_corr_nat line 441 source
lemma TateCurve.Blueprint.tsum_V_nat The Lambert-to-divisor-sum rearrangement: ∑_{n ≥ 0} qⁿ/(1 - qⁿ)² = ∑_{N ≥ 1} σ₁(N)qᴺ (the n = 0 term is junk 0) line 448 source
Source documentation
The Lambert-to-divisor-sum rearrangement: ∑_{n ≥ 0} qⁿ/(1 - qⁿ)² = ∑_{N ≥ 1} σ₁(N)qᴺ (the n = 0 term is junk 0).
```
private lemma tsum_V_nat {q : ℂ} (hq1 : ‖q‖ < 1) :
    ∑' n : ℕ, q ^ n / (1 - q ^ n) ^ 2 = sAn 1 q := by
…
```
Mentions: TateCurve.Blueprint.sAn
lemma TateCurve.Blueprint.summable_corr_int line 464 source
lemma TateCurve.Blueprint.tsum_corr_int The corrector sum over ℤ: ∑_{n : ℤ} qⁿ/(1 - qⁿ)² = 2∑_{N ≥ 1} σ₁(N)qᴺ (the n = 0 term is junk 0, and n ↔ -n are equal) line 474 source
Source documentation
The corrector sum over ℤ: ∑_{n : ℤ} qⁿ/(1 - qⁿ)² = 2∑_{N ≥ 1} σ₁(N)qᴺ (the n = 0 term is junk 0, and n ↔ -n are equal).
```
private lemma tsum_corr_int {q : ℂ} (hq0 : q ≠ 0) (hq1 : ‖q‖ < 1) :
    ∑' n : ℤ, q ^ n / (1 - q ^ n) ^ 2 = 2 * sAn 1 q := by
…
```
Mentions: TateCurve.Blueprint.sAn
lemma TateCurve.Blueprint.norm_mul_lt_one ‖qu‖ < 1 when ‖q‖ < ‖u‖ < 1 line 499 source
Source documentation
‖qu‖ < 1 when ‖q‖ < ‖u‖ < 1.
```
private lemma norm_mul_lt_one {u q : ℂ} (hqu : ‖q‖ < ‖u‖) (hu1 : ‖u‖ < 1) :
    ‖q * u‖ < 1 := by
…
```
lemma TateCurve.Blueprint.norm_mul_inv_lt_one ‖qu⁻¹‖ < 1 when 0 < ‖q‖ < ‖u‖ line 505 source
Source documentation
‖qu⁻¹‖ < 1 when 0 < ‖q‖ < ‖u‖.
```
private lemma norm_mul_inv_lt_one {u q : ℂ} (hq0 : 0 < ‖q‖) (hqu : ‖q‖ < ‖u‖) :
    ‖q * u⁻¹‖ < 1 := by
…
```
lemma TateCurve.Blueprint.zpow_neg_natCast_mul The substitution v ↦ v⁻¹ on v = qⁿu⁻¹ produces q⁻ⁿu line 511 source
Source documentation
The substitution v ↦ v⁻¹ on v = qⁿu⁻¹ produces q⁻ⁿu.
```
private lemma zpow_neg_natCast_mul (q u : ℂ) (n : ℕ) :
    q ^ (-(n : ℤ)) * u = (q ^ n * u⁻¹)⁻¹ := by
…
```
lemma TateCurve.Blueprint.summable_V Summability of the series defining XAn, for 0 < ‖q‖ < ‖u‖ < 1 line 516 source
Source documentation
Summability of the series defining XAn, for 0 < ‖q‖ < ‖u‖ < 1.
```
private lemma summable_V {u q : ℂ} (hq0 : q ≠ 0) (hqu : ‖q‖ < ‖u‖) (hu1 : ‖u‖ < 1) :
    Summable fun n : ℤ ↦ q ^ n * u / (1 - q ^ n * u) ^ 2 := by
…
```
lemma TateCurve.Blueprint.im_sub_int_mul_ne_zero For 0 < im z < im τ, every row z - nτ avoids the real axis line 532 source
Source documentation
For 0 < im z < im τ, every row z - nτ avoids the real axis.
```
private lemma im_sub_int_mul_ne_zero {τ z : ℂ} (hτ : 0 < τ.im) (hz : 0 < z.im)
    (hzτ : z.im < τ.im) (n : ℤ) : (z - n * τ).im ≠ 0 := by
…
```
lemma TateCurve.Blueprint.corrector_row_eval Documented declaration: corrector_row_eval line 542 source
Source documentation
The corrector rows of the ℘-expansion: ∑_{m : ℤ} (nτ + m)⁻² = (2πi)² V(qⁿ) + [n = 0]π²/3 where V(v) = v/(1-v)² (the row n = 0 is the Basel problem, and its V-term is junk 0).
```
private lemma corrector_row_eval {τ : ℂ} (hτ : 0 < τ.im) (n : ℤ) :
    ∑' m : ℤ, (((n * τ + m : ℂ)) ^ 2)⁻¹
      = (2 * (Real.pi : ℂ) * I) ^ 2 * (e τ ^ n / (1 - e τ ^ n) ^ 2)
        + if n = 0 then (Real.pi : ℂ) ^ 2 / 3 else 0 := by
…
```
Mentions: TateCurve.Blueprint.e
theorem TateCurve.Blueprint.weierstrassP_q_expansion Documented declaration: weierstrassP_q_expansion line 568 source
Source documentation
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 τ guarantees im (z - nτ) ≠ 0 for every n, so each row evaluates via sum_int_inv_sq': the row n contributes (2πi)² V(e(z - nτ)) - ∑_m (nτ + m)⁻² where V v = v/(1-v)², the corrector being 2ζ(2) = π²/3 for n = 0 (Basel) and (2πi)² V(qⁿ) for n ≠ 0. Summing over n, the first parts give (2πi)²(Xₐ + 2s₁(q)), the correctors give (2πi)² ⬝ 2s₁(q) + π²/3 (Lambert/divisor-sum rearrangement, tsum_corr_int), and -π²/3 = (2πi)²/12.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LT.lt, Real, OfNat.ofNat, Complex.im, Eq, PeriodPair.weierstrassP, TateCurve.Blueprint.periodPair, LT.lt.ne', HMul.hMul, HPow.hPow, Nat, Real.pi, Complex.I, HAdd.hAdd, HDiv.hDiv, TateCurve.Blueprint.XAn, TateCurve.Blueprint.e
Proof uses: Ne, TateCurve.Blueprint.e_ne_zero, Norm.norm, TateCurve.Blueprint.norm_e_lt_one, TateCurve.Blueprint.norm_e_lt_norm_e, LT.lt.trans, HasSum, Prod, Int, HSub.hSub, Inv.inv, Prod.fst, Prod.snd, SummationFilter.unconditional, Eq.mp, Subtype, Membership.mem, Submodule, PeriodPair.lattice, congrFun' and 120 more
172 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
theorem weierstrassP_q_expansion (τ : ℂ) (hτ : 0 < τ.im) (z : ℂ) (hz : 0 < z.im)
    (hzτ : z.im < τ.im) :
    ℘[periodPair τ hτ.ne'] z =
      (2 * (Real.pi : ℂ) * I) ^ 2 * (1 / 12 + XAn (e z) (e τ)) := by
…
```
Mentions: TateCurve.Blueprint.periodPair, TateCurve.Blueprint.XAn, TateCurve.Blueprint.e
lemma TateCurve.Blueprint.inv_sq_div_one_sub_inv_cube The rational-function identity (v⁻¹)²/(1 - v⁻¹)³ = -(v/(1 - v)³) for v ≠ 0 line 619 source
Source documentation
The rational-function identity (v⁻¹)²/(1 - v⁻¹)³ = -(v/(1 - v)³) for v ≠ 0.
```
private lemma inv_sq_div_one_sub_inv_cube {v : ℂ} (hv : v ≠ 0) :
    (v⁻¹) ^ 2 / (1 - v⁻¹) ^ 3 = -(v / (1 - v) ^ 3) := by
…
```
lemma TateCurve.Blueprint.inv_mul_one_add_inv_div_one_sub_inv_cube The rational-function identity v⁻¹(1 + v⁻¹)/(1 - v⁻¹)³ = -(v(1 + v)/(1 - v)³) for v ≠ 0: the function on the right-hand side of sum_int_inv_cube is odd under v ↦ v⁻¹ line 629 source
Source documentation
The rational-function identity v⁻¹(1 + v⁻¹)/(1 - v⁻¹)³ = -(v(1 + v)/(1 - v)³) for v ≠ 0: the function on the right-hand side of sum_int_inv_cube is odd under v ↦ v⁻¹.
```
private lemma inv_mul_one_add_inv_div_one_sub_inv_cube {v : ℂ} (hv : v ≠ 0) :
    v⁻¹ * (1 + v⁻¹) / (1 - v⁻¹) ^ 3 = -(v * (1 + v) / (1 - v) ^ 3) := by
…
```
lemma TateCurve.Blueprint.div_sq_add_two_mul_div_cube Documented declaration: div_sq_add_two_mul_div_cube line 639 source
Source documentation
The rational-function identity v/(1-v)² + 2v²/(1-v)³ = v(1+v)/(1-v)³ recombining the XAn and YAn summands into the ℘' row sums (also true at the junk value v = 1, where all terms are 0).
```
private lemma div_sq_add_two_mul_div_cube (v : ℂ) :
    v / (1 - v) ^ 2 + 2 * (v ^ 2 / (1 - v) ^ 3) = v * (1 + v) / (1 - v) ^ 3 := by
…
```
lemma TateCurve.Blueprint.sum_int_inv_cube' Extension of sum_int_inv_cube to w in the lower half plane line 649 source
Source documentation
Extension of sum_int_inv_cube to w in the lower half plane. In contrast to the square case, the row sum is odd under w ↦ -w, matching the oddness of v(1+v)/(1-v)³ under v ↦ v⁻¹.
```
private lemma sum_int_inv_cube' (w : ℂ) (hw : w.im ≠ 0) :
    ∑' m : ℤ, ((w + m) ^ 3)⁻¹ =
      -(2 * (Real.pi : ℂ) * I) ^ 3 / 2 * (e w * (1 + e w) / (1 - e w) ^ 3) := by
…
```
Mentions: TateCurve.Blueprint.e
lemma TateCurve.Blueprint.summable_V₂ Summability of the series defining YAn, for 0 < ‖q‖ < ‖u‖ < 1 line 659 source
Source documentation
Summability of the series defining YAn, for 0 < ‖q‖ < ‖u‖ < 1.
```
private lemma summable_V₂ {u q : ℂ} (hq0 : q ≠ 0) (hqu : ‖q‖ < ‖u‖) (hu1 : ‖u‖ < 1) :
    Summable fun n : ℤ ↦ (q ^ n * u) ^ 2 / (1 - q ^ n * u) ^ 3 := by
…
```
theorem TateCurve.Blueprint.derivWeierstrassP_q_expansion The q-expansion of ℘' (Silverman, Advanced topics, Theorem I.6.2): under the hypotheses of weierstrassP_q_expansion, ℘'(z; Λ_τ) = (2πi)³ (Xₐ(e z, e τ) + 2Yₐ(e z, e τ)) line 684 source
Source documentation
The q-expansion of ℘' (Silverman, Advanced topics, Theorem I.6.2): under the hypotheses of weierstrassP_q_expansion,
℘'(z; Λ_τ) = (2πi)³ (Xₐ(e z, e τ) + 2Yₐ(e z, e τ)).
Proof: as for weierstrassP_q_expansion, but simpler: group the absolutely convergent sum ℘'(z) = -2∑_ω (z - ω)⁻³ into rows ω = nτ + m (no regularising terms are needed here) and apply sum_int_inv_cube' to each row. The identity v/(1-v)² + 2v²/(1-v)³ = v(1+v)/(1-v)³ recombines the result into Xₐ + 2Yₐ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LT.lt, Real, OfNat.ofNat, Complex.im, Eq, PeriodPair.derivWeierstrassP, TateCurve.Blueprint.periodPair, LT.lt.ne', HMul.hMul, HPow.hPow, Nat, Real.pi, Complex.I, HAdd.hAdd, TateCurve.Blueprint.XAn, TateCurve.Blueprint.e, TateCurve.Blueprint.YAn
Proof uses: Ne, TateCurve.Blueprint.e_ne_zero, Norm.norm, TateCurve.Blueprint.norm_e_lt_one, TateCurve.Blueprint.norm_e_lt_norm_e, HasSum, Prod, Int, HDiv.hDiv, Neg.neg, HSub.hSub, Prod.fst, Prod.snd, SummationFilter.unconditional, PeriodPair.hasSum_derivWeierstrassP, Summable, Summable.congr, Inv.inv, Summable.mul_left, Mathlib.Meta.NormNum.isNat_le_true and 100 more
153 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem derivWeierstrassP_q_expansion (τ : ℂ) (hτ : 0 < τ.im) (z : ℂ) (hz : 0 < z.im)
    (hzτ : z.im < τ.im) :
    ℘'[periodPair τ hτ.ne'] z =
      (2 * (Real.pi : ℂ) * I) ^ 3 * (XAn (e z) (e τ) + 2 * YAn (e z) (e τ)) := by
…
```
Mentions: TateCurve.Blueprint.periodPair, TateCurve.Blueprint.XAn, TateCurve.Blueprint.e, TateCurve.Blueprint.YAn
lemma TateCurve.Blueprint.sum_int_inv_fourth Row sum, exponent 4: for w in the upper half plane, ∑_{m : ℤ} (w + m)⁻⁴ = (2πi)⁴/6 ⬝ ∑_{d ≥ 1} d³e(w)ᵈ line 726 source
Source documentation
Row sum, exponent 4: for w in the upper half plane, ∑_{m : ℤ} (w + m)⁻⁴ = (2πi)⁴/6 ⬝ ∑_{d ≥ 1} d³e(w)ᵈ. This is the case k = 3 of sum_int_inv_pow_succ.
```
private lemma sum_int_inv_fourth (w : ℂ) (hw : 0 < w.im) :
    ∑' m : ℤ, ((w + m) ^ 4)⁻¹
      = (2 * (Real.pi : ℂ) * I) ^ 4 / 6 * ∑' d : ℕ, (d : ℂ) ^ 3 * e w ^ d := by
…
```
Mentions: TateCurve.Blueprint.e
lemma TateCurve.Blueprint.hasSum_int_inv_fourth The Basel-type sum over ℤ in weight 4: ∑_{m : ℤ} m⁻⁴ = π⁴/45 line 735 source
Source documentation
The Basel-type sum over ℤ in weight 4: ∑_{m : ℤ} m⁻⁴ = π⁴/45.
```
private lemma hasSum_int_inv_fourth :
    HasSum (fun m : ℤ ↦ ((m : ℂ) ^ 4)⁻¹) ((Real.pi : ℂ) ^ 4 / 45) := by
…
```
lemma TateCurve.Blueprint.not_summable_natCast_pow ∑ dᵏ diverges; used to see that the Lambert series contributes junk 0 in the n = 0 row line 743 source
Source documentation
∑ dᵏ diverges; used to see that the Lambert series contributes junk 0 in the n = 0 row.
```
private lemma not_summable_natCast_pow (k : ℕ) : ¬ Summable fun d : ℕ ↦ (d : ℂ) ^ k := by
…
```
lemma TateCurve.Blueprint.tsum_natCast_pow_mul_one The junk value of the Lambert series in the row n = 0: ∑_{d ≥ 0} dʲ ⬝ 1ᵈ = 0, since the series diverges line 756 source
Source documentation
The junk value of the Lambert series in the row n = 0: ∑_{d ≥ 0} dʲ ⬝ 1ᵈ = 0, since the series diverges.
```
private lemma tsum_natCast_pow_mul_one (j : ℕ) :
    ∑' d : ℕ, (d : ℂ) ^ j * (1 : ℂ) ^ d = 0 := by
…
```
lemma TateCurve.Blueprint.tsum_tsum_pow_eq_sAn The divisor-sum rearrangement ∑_{n ≥ 0} ∑_{d ≥ 0} dʲ q^{nd} = sⱼ(q) for ‖q‖ < 1 and j ≠ 0 (the row n = 0 is junk 0, and the terms d = 0 vanish) line 762 source
Source documentation
The divisor-sum rearrangement ∑_{n ≥ 0} ∑_{d ≥ 0} dʲ q^{nd} = sⱼ(q) for ‖q‖ < 1 and j ≠ 0 (the row n = 0 is junk 0, and the terms d = 0 vanish).
```
private lemma tsum_tsum_pow_eq_sAn {q : ℂ} (hq1 : ‖q‖ < 1) {j : ℕ} (hj : j ≠ 0) :
    ∑' n : ℕ, ∑' d : ℕ, (d : ℂ) ^ j * (q ^ n) ^ d = sAn j q := by
…
```
Mentions: TateCurve.Blueprint.sAn
lemma TateCurve.Blueprint.tsum_int_lambert_natAbs The two-tailed version: ∑_{n : ℤ} ∑_{d ≥ 0} dʲ q^{|n|d} = 2sⱼ(q) for ‖q‖ < 1 and j ≠ 0, given summability of the rows line 776 source
Source documentation
The two-tailed version: ∑_{n : ℤ} ∑_{d ≥ 0} dʲ q^{|n|d} = 2sⱼ(q) for ‖q‖ < 1 and j ≠ 0, given summability of the rows.
```
private lemma tsum_int_lambert_natAbs {q : ℂ} (hq1 : ‖q‖ < 1) {j : ℕ} (hj : j ≠ 0)
    (hL : Summable fun n : ℤ ↦ ∑' d : ℕ, (d : ℂ) ^ j * (q ^ n.natAbs) ^ d) :
    ∑' n : ℤ, ∑' d : ℕ, (d : ℂ) ^ j * (q ^ n.natAbs) ^ d = 2 * sAn j q := by
…
```
Mentions: TateCurve.Blueprint.sAn

lemma TateCurve.Blueprint.row_eval_ne_zero Rows n ≠ 0 of an even-weight lattice sum, via a row-sum identity hrow valid on the upper half plane (evenness reduces n < 0 to n > 0) line 799 source

Source documentation

Rows n ≠ 0 of an even-weight lattice sum, via a row-sum identity hrow valid on the upper half plane (evenness reduces n < 0 to n > 0).

private lemma row_eval_ne_zero {τ : ℂ} (hτ : 0 < τ.im) {k j : ℕ} (hkeven : Even k) {C : ℂ}
    (hrow : ∀ w : ℂ, 0 < w.im →
      ∑' m : ℤ, ((w + m) ^ k)⁻¹ = C * ∑' d : ℕ, (d : ℂ) ^ j * e w ^ d)
    {n : ℤ} (hn : n ≠ 0) :
    ∑' m : ℤ, (((n : ℂ) * τ + m) ^ k)⁻¹
      = C * ∑' d : ℕ, (d : ℂ) ^ j * (e τ ^ n.natAbs) ^ d := by
…

Mentions: TateCurve.Blueprint.e

lemma TateCurve.Blueprint.G_q_expansion Documented declaration: G_q_expansion line 822 source
Source documentation
Common core of g₂_q_expansion and g₃_q_expansion: the q-expansion of the Eisenstein lattice sum G k = ∑_{ω ∈ Λ_τ} ω⁻ᵏ for even k > 2, given the row-sum identity with constant C (which is (2πi)ᵏ/(k-1)!) and the value Z of the row n = 0 (which is 2ζ(k)). Reindex the lattice sum by ℤ × ℤ, evaluate the rows (row_eval_ne_zero), and sum over n by Fubini and the divisor-sum rearrangement (tsum_int_lambert_natAbs), giving the coefficients σⱼ, j = k - 1.
```
private lemma G_q_expansion (τ : ℂ) (hτ : 0 < τ.im) {k j : ℕ} (hj : j ≠ 0) (hk : 2 < k)
    (hkeven : Even k) {C Z : ℂ} (hC : C ≠ 0)
    (hrow : ∀ w : ℂ, 0 < w.im →
      ∑' m : ℤ, ((w + m) ^ k)⁻¹ = C * ∑' d : ℕ, (d : ℂ) ^ j * e w ^ d)
    (hZ : HasSum (fun m : ℤ ↦ ((m : ℂ) ^ k)⁻¹) Z) :
    (periodPair τ hτ.ne').G k = Z + 2 * C * sAn j (e τ) := by
…
```
Mentions: TateCurve.Blueprint.e, TateCurve.Blueprint.periodPair, TateCurve.Blueprint.sAn
theorem TateCurve.Blueprint.g₂_q_expansion The q-expansion of g₂ (Silverman, Advanced topics, Theorem I.7.1): g₂(Λ_τ) = (2πi)⁴/12 ⬝ (1 + 240s₃(q)) line 868 source
Source documentation
The q-expansion of g₂ (Silverman, Advanced topics, Theorem I.7.1):
g₂(Λ_τ) = (2πi)⁴/12 ⬝ (1 + 240s₃(q)).
This is g₂ = 60G₄ and the case k = 4 of G_q_expansion, with row-sum identity sum_int_inv_fourth and 2ζ(4) = π⁴/45 (hasSum_int_inv_fourth).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LT.lt, Real, OfNat.ofNat, Complex.im, Eq, PeriodPair.g₂, TateCurve.Blueprint.periodPair, LT.lt.ne', HMul.hMul, HDiv.hDiv, HPow.hPow, Nat, Real.pi, Complex.I, HAdd.hAdd, TateCurve.Blueprint.sAn, TateCurve.Blueprint.e
Proof uses: Eq.mpr, PeriodPair.G, id, congrArg, PeriodPair.g₂.eq_1, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Mathlib.Meta.NormNum.isNat_lt_true, Exists.intro, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_add, div_ne_zero, pow_ne_zero, TateCurve.Blueprint.two_pi_I_ne_zero, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.cast_zero, Mathlib.Tactic.Ring.of_eq and 69 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem g₂_q_expansion (τ : ℂ) (hτ : 0 < τ.im) :
    (periodPair τ hτ.ne').g₂ =
      (2 * (Real.pi : ℂ) * I) ^ 4 / 12 * (1 + 240 * sAn 3 (e τ)) := by
…
```
Mentions: TateCurve.Blueprint.periodPair, TateCurve.Blueprint.sAn, TateCurve.Blueprint.e
theorem TateCurve.Blueprint.bernoulli'_five line 880 source
theorem TateCurve.Blueprint.bernoulli'_six line 884 source
theorem TateCurve.Blueprint.riemannZeta_six The value ζ(6) = π⁶/945 (companion to Mathlib's riemannZeta_four) line 890 source
Source documentation
The value ζ(6) = π⁶/945 (companion to Mathlib's riemannZeta_four).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Complex, riemannZeta, OfNat.ofNat, Nat, HDiv.hDiv, HPow.hPow, Real.pi
Proof uses: HMul.hMul, Neg.neg, HAdd.hAdd, HSub.hSub, bernoulli, Nat.factorial, riemannZeta_two_mul_nat, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Eq.mpr, id, congrArg, Eq.mp, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_natCast and 66 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem riemannZeta_six : riemannZeta 6 = (π : ℂ) ^ 6 / 945 := by
…
```
lemma TateCurve.Blueprint.sum_int_inv_sixth Row sum, exponent 6: for w in the upper half plane, ∑_{m : ℤ} (w + m)⁻⁶ = (2πi)⁶/120 ⬝ ∑_{d ≥ 1} d⁵e(w)ᵈ line 900 source
Source documentation
Row sum, exponent 6: for w in the upper half plane, ∑_{m : ℤ} (w + m)⁻⁶ = (2πi)⁶/120 ⬝ ∑_{d ≥ 1} d⁵e(w)ᵈ. This is the case k = 5 of sum_int_inv_pow_succ.
```
private lemma sum_int_inv_sixth (w : ℂ) (hw : 0 < w.im) :
    ∑' m : ℤ, ((w + m) ^ 6)⁻¹
      = (2 * (Real.pi : ℂ) * I) ^ 6 / 120 * ∑' d : ℕ, (d : ℂ) ^ 5 * e w ^ d := by
…
```
Mentions: TateCurve.Blueprint.e
lemma TateCurve.Blueprint.hasSum_int_inv_sixth The Basel-type sum over ℤ in weight 6: ∑_{m : ℤ} m⁻⁶ = 2ζ(6) = 2π⁶/945 line 909 source
Source documentation
The Basel-type sum over ℤ in weight 6: ∑_{m : ℤ} m⁻⁶ = 2ζ(6) = 2π⁶/945.
```
private lemma hasSum_int_inv_sixth :
    HasSum (fun m : ℤ ↦ ((m : ℂ) ^ 6)⁻¹) (2 * ((Real.pi : ℂ) ^ 6 / 945)) := by
…
```
theorem TateCurve.Blueprint.g₃_q_expansion The q-expansion of g₃ (Silverman, Advanced topics, Theorem I.7.1): g₃(Λ_τ) = -(2πi)⁶/216 ⬝ (1 - 504s₅(q)) line 920 source
Source documentation
The q-expansion of g₃ (Silverman, Advanced topics, Theorem I.7.1):
g₃(Λ_τ) = -(2πi)⁶/216 ⬝ (1 - 504s₅(q)).
This is g₃ = 140G₆ and the case k = 6 of G_q_expansion, with row-sum identity sum_int_inv_sixth and 2ζ(6) = 2π⁶/945 (hasSum_int_inv_sixth).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LT.lt, Real, OfNat.ofNat, Complex.im, Eq, PeriodPair.g₃, TateCurve.Blueprint.periodPair, LT.lt.ne', HMul.hMul, HDiv.hDiv, Neg.neg, HPow.hPow, Nat, Real.pi, Complex.I, HSub.hSub, TateCurve.Blueprint.sAn, TateCurve.Blueprint.e
Proof uses: Eq.mpr, PeriodPair.G, id, congrArg, PeriodPair.g₃.eq_1, HAdd.hAdd, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Mathlib.Meta.NormNum.isNat_lt_true, Exists.intro, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_add, div_ne_zero, pow_ne_zero, TateCurve.Blueprint.two_pi_I_ne_zero, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.cast_zero and 79 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem g₃_q_expansion (τ : ℂ) (hτ : 0 < τ.im) :
    (periodPair τ hτ.ne').g₃ =
      -(2 * (Real.pi : ℂ) * I) ^ 6 / 216 * (1 - 504 * sAn 5 (e τ)) := by
…
```
Mentions: TateCurve.Blueprint.periodPair, TateCurve.Blueprint.sAn, TateCurve.Blueprint.e
theorem TateCurve.Blueprint.log_div_two_pi_I_im line 934 source
theorem TateCurve.Blueprint.e_log_div_two_pi_I line 940 source
theorem TateCurve.Blueprint.notMem_lattice_of_im_between line 948 source
theorem TateCurve.Blueprint.analytic_weierstrass_algebra line 964 source
theorem TateCurve.Blueprint.analytic_weierstrass_of_exp line 981 source
theorem TateCurve.Blueprint.analytic_weierstrass The analytic form of the main theorem (Silverman, Advanced topics, Theorem V.1.1(a)): for 0 < ‖q‖ < ‖u‖ < 1, Yₐ² + XₐYₐ = Xₐ³ - 5s₃(q)Xₐ - (5s₃(q) + 7s₅(q))/12 line 1002 source
Source documentation
The analytic form of the main theorem (Silverman, Advanced topics, Theorem V.1.1(a)): for 0 < ‖q‖ < ‖u‖ < 1,
Yₐ² + XₐYₐ = Xₐ³ - 5s₃(q)Xₐ - (5s₃(q) + 7s₅(q))/12.
Proof sketch: the hypotheses ensure u ∉ qᶻ, and we may choose z, τ with e z = u, e τ = q, 0 < im z < im τ (so z ∉ Λ_τ). Substitute the four q-expansions into the differential equation ℘'² = 4℘³ - g₂℘ - g₃ (PeriodPair.derivWeierstrassP_sq) and divide by (2πi)⁶ and by 4 (analytic_weierstrass_algebra).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LT.lt, Real, OfNat.ofNat, Norm.norm, Eq, HAdd.hAdd, HPow.hPow, Nat, TateCurve.Blueprint.YAn, HMul.hMul, TateCurve.Blueprint.XAn, HSub.hSub, TateCurve.Blueprint.sAn, HDiv.hDiv
Proof uses: Complex.im, Complex.log, Real.pi, Complex.I, Eq.mpr, Neg.neg, Real.log, id, congrArg, div_pos, Iff.mpr, neg_pos, Real.log_neg_iff, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble and 8 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem analytic_weierstrass {u q : ℂ} (h0 : 0 < ‖q‖) (h1 : ‖q‖ < ‖u‖) (h2 : ‖u‖ < 1) :
    YAn u q ^ 2 + XAn u q * YAn u q =
      XAn u q ^ 3 - 5 * sAn 3 q * XAn u q - (5 * sAn 3 q + 7 * sAn 5 q) / 12 := by
…
```
Mentions: TateCurve.Blueprint.YAn, TateCurve.Blueprint.XAn, TateCurve.Blueprint.sAn
def TateCurve.Blueprint.evalAt Evaluation of a rational function in ℚ(u) at a complex number, with junk value 0 at the (finitely many) poles line 1024 source
Source documentation
Evaluation of a rational function in ℚ(u) at a complex number, with junk value 0 at the (finitely many) poles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, RatFunc, Rat
Proof uses: RatFunc.eval, Algebra.algebraMap
10 instances, coercions and auxiliary constants left out.
```
def evalAt (u : ℂ) (r : RatFunc ℚ) : ℂ := r.eval (algebraMap ℚ ℂ) u
```
def TateCurve.Blueprint.evalAtHom For transcendental u, evaluation at u is a ring homomorphism ℚ(u) →+* ℂ (there are no poles to produce junk values) line 1028 source
Source documentation
For transcendental u, evaluation at u is a ring homomorphism ℚ(u) →+* ℂ (there are no poles to produce junk values).
```
private noncomputable def evalAtHom (u : ℂ) (hu : Transcendental ℚ u) : RatFunc ℚ →+* ℂ where
…
```
theorem TateCurve.Blueprint.evalAtHom_apply line 1035 source
theorem TateCurve.Blueprint.evalAtHom_ratFuncX line 1040 source
lemma TateCurve.Blueprint.hasSum_pnat_of_nat line 1047 source
lemma TateCurve.Blueprint.hasSum_nat_of_pnat_add line 1054 source
lemma TateCurve.Blueprint.tsum_int_decomp Splitting a summable ℤ-indexed sum into the term at 0 and the two tails line 1065 source
Source documentation
Splitting a summable ℤ-indexed sum into the term at 0 and the two tails.
```
private lemma tsum_int_decomp {f : ℤ → ℂ} (hf : Summable f) :
    ∑' n : ℤ, f n
      = f 0 + ∑' n : ℕ+, f ((n : ℕ) : ℤ) + ∑' n : ℕ+, f (-((n : ℕ) : ℤ)) := by
…
```
lemma TateCurve.Blueprint.hasSum_pnat_lambert₁ line 1080 source
lemma TateCurve.Blueprint.hasSum_pnat_lambert₂ line 1084 source
lemma TateCurve.Blueprint.hasSum_pnat_lambert₂' line 1089 source
lemma TateCurve.Blueprint.norm_pow_mul_lt_one If ‖q‖ < 1 and ‖q * y‖ < 1 then ‖qⁿy‖ < 1 for every n ≥ 1 line 1108 source
Source documentation
If ‖q‖ < 1 and ‖q * y‖ < 1 then ‖qⁿy‖ < 1 for every n ≥ 1.
```
private lemma norm_pow_mul_lt_one {q y : ℂ} (hq1 : ‖q‖ < 1) (hqy : ‖q * y‖ < 1) (n : ℕ+) :
    ‖q ^ (n : ℕ) * y‖ < 1 := by
…
```
lemma TateCurve.Blueprint.cast_le_sq line 1115 source
lemma TateCurve.Blueprint.choose_two_le_sq line 1120 source
lemma TateCurve.Blueprint.choose_add_one_two_le_sq line 1124 source
lemma TateCurve.Blueprint.summable_coeff_prod Geometric-decay summability of the double series ∑ a(m)yᵐq^{nm}, for any coefficients of at most quadratic growth line 1134 source
Source documentation
Geometric-decay summability of the double series ∑ a(m)yᵐq^{nm}, for any coefficients of at most quadratic growth.
```
private lemma summable_coeff_prod {a : ℕ → ℂ} {x y : ℂ}
    (ha : ∀ m : ℕ+, ‖a (m : ℕ)‖ ≤ (((m : ℕ)) : ℝ) ^ 2) (hx : ‖x‖ < 1) (hxy : ‖x * y‖ < 1) :
    Summable fun p : ℕ+ × ℕ+ ↦ a (p.2 : ℕ) * y ^ (p.2 : ℕ) * x ^ ((p.1 : ℕ) * (p.2 : ℕ)) := by
…
```
lemma TateCurve.Blueprint.hasSum_prod_pnat A summable double series over ℕ+ × ℕ+ has sum the iterated sum of its rows line 1151 source
Source documentation
A summable double series over ℕ+ × ℕ+ has sum the iterated sum of its rows.
```
private lemma hasSum_prod_pnat {T : ℕ+ × ℕ+ → ℂ} {F : ℕ+ → ℂ}
    (hsum : Summable T) (hfib : ∀ n : ℕ+, HasSum (fun m : ℕ+ ↦ T (n, m)) (F n)) :
    HasSum T (∑' n : ℕ+, F n) := by
…
```

lemma TateCurve.Blueprint.hasSum_prod_lambert Fubini for the Lambert-type double series with coefficients a of at most quadratic growth, whose rows sum in closed form to g (qⁿy) line 1159 source

Source documentation

Fubini for the Lambert-type double series with coefficients a of at most quadratic growth, whose rows sum in closed form to g (qⁿy).

private lemma hasSum_prod_lambert {q y : ℂ} (a : ℕ → ℂ) (g : ℂ → ℂ)
    (ha : ∀ m : ℕ+, ‖a (m : ℕ)‖ ≤ (((m : ℕ)) : ℝ) ^ 2) (hq1 : ‖q‖ < 1) (hqy : ‖q * y‖ < 1)
    (hg : ∀ v : ℂ, ‖v‖ < 1 → HasSum (fun m : ℕ+ ↦ a (m : ℕ) * v ^ (m : ℕ)) (g v)) :
    HasSum (fun p : ℕ+ × ℕ+ ↦ a (p.2 : ℕ) * y ^ (p.2 : ℕ) * q ^ ((p.1 : ℕ) * (p.2 : ℕ)))
      (∑' n : ℕ+, g (q ^ (n : ℕ) * y)) :=
…

lemma TateCurve.Blueprint.hasSum_divisor_collect Collecting a double series ∑_{n,m} g(m)x^{nm} by powers of x: the coefficient of x^N is the divisor sum ∑_{d ∣ N} g d line 1169 source
Source documentation
Collecting a double series ∑_{n,m} g(m)x^{nm} by powers of x: the coefficient of x^N is the divisor sum ∑_{d ∣ N} g d.
```
private lemma hasSum_divisor_collect (g : ℕ → ℂ) {x : ℂ} {S : ℂ}
    (hT : HasSum (fun p : ℕ+ × ℕ+ ↦ g (p.2 : ℕ) * x ^ ((p.1 : ℕ) * (p.2 : ℕ))) S) :
    HasSum (fun N : ℕ+ ↦ (∑ d ∈ (N : ℕ).divisors, g d) * x ^ (N : ℕ)) S := by
…
```
lemma TateCurve.Blueprint.hasSum_prodC The y = 1 double series, with the divisor sums already recognised as s₁ line 1191 source
Source documentation
The y = 1 double series, with the divisor sums already recognised as s₁.
```
private lemma hasSum_prodC {q : ℂ} (hq1 : ‖q‖ < 1) :
    HasSum (fun p : ℕ+ × ℕ+ ↦
        ((p.2 : ℕ) : ℂ) * (1 : ℂ) ^ (p.2 : ℕ) * q ^ ((p.1 : ℕ) * (p.2 : ℕ)))
      (sAn 1 q) := by
…
```
Mentions: TateCurve.Blueprint.sAn
theorem TateCurve.Blueprint.coeff_X_of_ne line 1203 source
theorem TateCurve.Blueprint.evalAt_coeff_X_zero line 1208 source
theorem TateCurve.Blueprint.evalAt_coeff_X line 1212 source
theorem TateCurve.Blueprint.coeff_Y_of_ne line 1219 source
theorem TateCurve.Blueprint.evalAt_coeff_Y_zero line 1225 source
theorem TateCurve.Blueprint.evalAt_coeff_Y line 1229 source
theorem TateCurve.Blueprint.hasSum_X_eval Documented declaration: hasSum_X_eval line 1250 source
Source documentation
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 - qⁿu)² = ∑_{m ≥ 1} m qⁿᵐuᵐ (geometric series, ‖qⁿu‖ < 1); for n ≤ -1 with N = -n, the rational-function identity v/(1-v)² = v⁻¹/(1-v⁻¹)² gives qⁿu/(1 - qⁿu)² = ∑_{m ≥ 1} m qᴺᵐu⁻ᵐ (‖qᴺu⁻¹‖ < 1); and -2s₁(q) = -2∑_N (∑_{d ∣ N} d) qᴺ. All double series converge absolutely (summable_coeff_prod), so they may be collected by powers of q (hasSum_divisor_collect), and the coefficient of qᴺ is exactly ∑_{d ∣ N} d(uᵈ + u⁻ᵈ - 2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Transcendental, Rat, LT.lt, Real, OfNat.ofNat, Norm.norm, HasSum, Nat, HMul.hMul, TateCurve.Blueprint.evalAt, LinearMap, RatFunc, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, TateCurve.X, HPow.hPow, TateCurve.Blueprint.XAn and 1 more
Proof uses: Ne, Iff.mp, norm_pos_iff, LT.lt.trans, Prod, PNat, Prod.snd, Prod.fst, tsum, HDiv.hDiv, HSub.hSub, Inv.inv, Finset.sum, Nat.divisors, HAdd.hAdd, TateCurve.Blueprint.sAn, HasSum.congr_fun, HasSum.sub, HasSum.add, HasSum.mul_left and 95 more
202 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem hasSum_X_eval {u q : ℂ} (hu : Transcendental ℚ u) (h0 : 0 < ‖q‖)
    (h1 : ‖q‖ < ‖u‖) (h2 : ‖u‖ < 1) :
    HasSum (fun n : ℕ ↦ evalAt u ((PowerSeries.coeff n) X) * q ^ n) (XAn u q) := by
…
```
Mentions: TateCurve.Blueprint.evalAt, TateCurve.X, TateCurve.Blueprint.XAn
theorem TateCurve.Blueprint.hasSum_Y_eval 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) line 1289 source
Source documentation
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+1) choose 2) vᵐ for the rows n ≤ -1, and s₁(q) = ∑_N (∑_{d ∣ N} d) qᴺ for the correction term.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Transcendental, Rat, LT.lt, Real, OfNat.ofNat, Norm.norm, HasSum, Nat, HMul.hMul, TateCurve.Blueprint.evalAt, LinearMap, RatFunc, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, TateCurve.Y, HPow.hPow, TateCurve.Blueprint.YAn and 1 more
Proof uses: Ne, Iff.mp, norm_pos_iff, LT.lt.trans, Prod, PNat, Nat.choose, Prod.snd, Prod.fst, tsum, HDiv.hDiv, HSub.hSub, HAdd.hAdd, Inv.inv, Finset.sum, Nat.divisors, TateCurve.Blueprint.sAn, HasSum.congr_fun, HasSum.add, HasSum.sub and 96 more
200 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem hasSum_Y_eval {u q : ℂ} (hu : Transcendental ℚ u) (h0 : 0 < ‖q‖)
    (h1 : ‖q‖ < ‖u‖) (h2 : ‖u‖ < 1) :
    HasSum (fun n : ℕ ↦ evalAt u ((PowerSeries.coeff n) Y) * q ^ n) (YAn u q) := by
…
```
Mentions: TateCurve.Blueprint.evalAt, TateCurve.Y, TateCurve.Blueprint.YAn
theorem TateCurve.Blueprint.evalAt_ratCast line 1327 source
theorem TateCurve.Blueprint.summable_sAn_terms line 1331 source
theorem TateCurve.Blueprint.ofNat_powerSeries_eq_C line 1339 source
theorem TateCurve.Blueprint.coeff_a₆ line 1344 source
theorem TateCurve.Blueprint.evalAt_coeff_a₆ line 1351 source
theorem TateCurve.Blueprint.coeff_a₄ line 1356 source
theorem TateCurve.Blueprint.evalAt_coeff_a₄ line 1364 source
theorem TateCurve.Blueprint.hasSum_a₄_eval The coefficients of the formal series a₄ evaluated at any u sum to -5s₃(q) for ‖q‖ < 1 line 1371 source
Source documentation
The coefficients of the formal series a₄ evaluated at any u sum to -5s₃(q) for ‖q‖ < 1. (The coefficients are constants, so this is just the convergence of ∑ σ₃(n)qⁿ.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LT.lt, Real, Norm.norm, OfNat.ofNat, HasSum, Nat, HMul.hMul, TateCurve.Blueprint.evalAt, LinearMap, RatFunc, Rat, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, TateCurve.a₄, HPow.hPow, Neg.neg, TateCurve.Blueprint.sAn and 1 more
Proof uses: HasSum.congr_fun, ArithmeticFunction, ArithmeticFunction.sigma, tsum, HasSum.mul_left, Summable.hasSum, Eq.mpr, Eq, id, congrArg, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos and 32 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem hasSum_a₄_eval (u : ℂ) {q : ℂ} (hq : ‖q‖ < 1) :
    HasSum (fun n : ℕ ↦ evalAt u ((PowerSeries.coeff n) a₄) * q ^ n) (-5 * sAn 3 q) :=
…
```
Mentions: TateCurve.Blueprint.evalAt, TateCurve.a₄, TateCurve.Blueprint.sAn
theorem TateCurve.Blueprint.hasSum_a₆_eval The coefficients of the formal series a₆ evaluated at any u sum to -(5s₃(q) + 7s₅(q))/12 for ‖q‖ < 1 line 1378 source
Source documentation
The coefficients of the formal series a₆ evaluated at any u sum to -(5s₃(q) + 7s₅(q))/12 for ‖q‖ < 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LT.lt, Real, Norm.norm, OfNat.ofNat, HasSum, Nat, HMul.hMul, TateCurve.Blueprint.evalAt, LinearMap, RatFunc, Rat, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, TateCurve.a₆, HPow.hPow, HDiv.hDiv, Neg.neg and 3 more
Proof uses: HasSum.congr_fun, ArithmeticFunction, ArithmeticFunction.sigma, tsum, HasSum.div_const, HasSum.neg, HasSum.add, HasSum.mul_left, Summable.hasSum, Eq.mpr, Eq, id, congrArg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Rat.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.div_congr, Int.rawCast and 55 more
150 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem hasSum_a₆_eval (u : ℂ) {q : ℂ} (hq : ‖q‖ < 1) :
    HasSum (fun n : ℕ ↦ evalAt u ((PowerSeries.coeff n) a₆) * q ^ n)
      (-(5 * sAn 3 q + 7 * sAn 5 q) / 12) :=
…
```
Mentions: TateCurve.Blueprint.evalAt, TateCurve.a₆, TateCurve.Blueprint.sAn
theorem TateCurve.Blueprint.coeffs_eq_zero_of_hasSum_punctured line 1387 source
theorem TateCurve.Blueprint.ratFunc_eq_zero_of_evalAt_eq_zero_on_infinite line 1405 source
theorem TateCurve.Blueprint.eq_zero_of_forall_hasSum_zero Documented declaration: eq_zero_of_forall_hasSum_zero line 1431 source
Source documentation
The descent lemma: a formal power series F ∈ ℚ(u)⟦q⟧ vanishes provided that, for infinitely many u₀ : ℂ, the evaluated series ∑ₙ Fₙ(u₀)q₀ⁿ converges with sum 0 for all sufficiently small nonzero q₀.
Proof sketch: fix u₀. The function q₀ ↦ ∑ₙ Fₙ(u₀)q₀ⁿ is analytic on ‖q₀‖ < r (a power series converging pointwise on a disc is analytic there) and vanishes on the punctured disc, hence at 0 by continuity; by uniqueness of power series coefficients, Fₙ(u₀) = 0 for all n. So for each n the rational function Fₙ vanishes at infinitely many points of ℂ (junk values at the finitely many poles of Fₙ do not matter, as removing them leaves an infinite set), hence its numerator has infinitely many roots and Fₙ = 0 (Polynomial.eq_zero_of_infinite_isRoot).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, RatFunc, Rat, Set, Complex, Set.Infinite, Membership.mem, Exists, Real, And, GT.gt, OfNat.ofNat, LT.lt, Norm.norm, HasSum, Nat, HMul.hMul, TateCurve.Blueprint.evalAt, LinearMap, RingHom.id and 5 more
Proof uses: PowerSeries.ext, congrFun
77 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem eq_zero_of_forall_hasSum_zero (F : (RatFunc ℚ)⟦X⟧) (S : Set ℂ) (hS : S.Infinite)
    (h : ∀ u ∈ S, ∃ r > 0, ∀ q : ℂ, 0 < ‖q‖ → ‖q‖ < r →
      HasSum (fun n : ℕ ↦ evalAt u ((PowerSeries.coeff n) F) * q ^ n) 0) : F = 0 := by
…
```
Mentions: TateCurve.X, TateCurve.Blueprint.evalAt
theorem TateCurve.Blueprint.hasSum_evalAt_add line 1440 source
theorem TateCurve.Blueprint.hasSum_evalAt_neg line 1452 source
theorem TateCurve.Blueprint.hasSum_evalAt_sub line 1461 source
theorem TateCurve.Blueprint.hasSum_evalAt_mul line 1468 source
theorem TateCurve.Blueprint.transcendental_punctured_unit_disk_infinite line 1484 source
theorem TateCurve.weierstrass_equation The point (X(u,q), Y(u,q)) satisfies the Weierstrass equation y² + xy = x³ + a₄x + a₆ of the Tate curve, as an identity in ℚ(u)⟦q⟧ line 1527 source
Source documentation
The point (X(u,q), Y(u,q)) satisfies the Weierstrass equation y² + xy = x³ + a₄x + a₆ of the Tate curve, as an identity in ℚ(u)⟦q⟧.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, PowerSeries, RatFunc, Rat, HAdd.hAdd, Unit, HPow.hPow, Nat, TateCurve.Y, OfNat.ofNat, HMul.hMul, TateCurve.X, TateCurve.a₄, TateCurve.a₆
Proof uses: Eq.mpr, HSub.hSub, id, congrArg, Eq.symm, propext, sub_eq_zero, TateCurve.Blueprint.eq_zero_of_forall_hasSum_zero, Set.ofPred, Complex, And, Transcendental, LT.lt, Real, Norm.norm, Membership.mem, Set, Exists.intro, GT.gt, HasSum and 114 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem weierstrass_equation : Y ^ 2 + X * Y = X ^ 3 + a₄ * X + a₆ := by
…
```
Mentions: TateCurve.Y, TateCurve.X, TateCurve.a₄, TateCurve.a₆