Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 9 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

9 results

Clear filters
Project-declaredLean 4.32.0

Analytic weierstrass

TateCurve.Blueprint.analytic_weierstrass

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

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Deriv Weierstrass P q expansion

TateCurve.Blueprint.derivWeierstrassP_q_expansion

Plain-language statement

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

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Eq zero of forall has Sum zero

TateCurve.Blueprint.eq_zero_of_forall_hasSum_zero

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

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

G₂ q expansion

TateCurve.Blueprint.g₂_q_expansion

Plain-language statement

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

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

G₃ q expansion

TateCurve.Blueprint.g₃_q_expansion

Plain-language statement

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

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Has Sum X eval

TateCurve.Blueprint.hasSum_X_eval

Plain-language statement

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

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record