Documentation

FormalConjectures.Wikipedia.EllipticCurveRank

Some conjectures about ranks of elliptic curves over ℚ #

References:

[PPVW2016] Jennifer Park, Bjorn Poonen, John Voight, and Melanie Matchett Wood. A heuristic for boundedness of ranks of elliptic curves, https://ems.press/journals/jems/articles/16228
[BS2013] Manjul Bhargava and Arul Shankar. The average size of the 5-Selmer group of elliptic curves is 6, and the average rank is less than 1, https://arxiv.org/pdf/1312.7859
Wikipedia

structure EllipticCurveRank.RatEllipticCurve :

A data structure representing isomoprhism classes of elliptic curves over ℚ. Every elliptic curve over ℚ is isomorphic to one with Weierstrass equation y² = x³ + Ax + B, and the pair (A,B) is unique if it satisfy the reduced condition below. See Section 5.1 in [PPVW2016].

A : ℤ
B : ℤ
reduced (p : ℕ) : Nat.Prime p → ¬(↑p ^ 4 ∣ self.A ∧ ↑p ^ 6 ∣ self.B)
Δ_ne_zero : 4 * self.A ^ 3 + 27 * self.B ^ 2 ≠ 0

Instances For

instance EllipticCurveRank.instFiniteIntPointBaseChangeOfNumberFieldOfIsElliptic_formalConjectures {K : Type u_1} [Field K] [NumberField K] (E : WeierstrassCurve K) [E.IsElliptic] :

Module.Finite ℤ (WeierstrassCurve.Affine.Point (E.baseChange K))

The rank of an elliptic curve over a number field is always finite by the Mordell–Weil theorem. Consequently, the rank is always finite, so finrank ℤ E⟮K⟯ = 0 really means that the group of rational points is torsion, not that it is of infinite rank.

def EllipticCurveRank.RatEllipticCurve.toWeierstrass (E : RatEllipticCurve) :

WeierstrassCurve ℚ

Convert the structure RatEllipticCurve to a Weierstrass curve.

Equations

E.toWeierstrass = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := ↑E.A, a₆ := ↑E.B }

Instances For

@[reducible, inline]

noncomputable abbrev EllipticCurveRank.RatEllipticCurve.rank (E : RatEllipticCurve) :

The rank of an elliptic curve over ℚ.

Equations

E.rank = Module.finrank ℤ (WeierstrassCurve.Affine.Point (E.toWeierstrass.baseChange ℚ))

Instances For

instance EllipticCurveRank.RatEllipticCurve.instIsEllipticRatToWeierstrass (E : RatEllipticCurve) :

E.toWeierstrass.IsElliptic

def EllipticCurveRank.RatEllipticCurve.naiveHeight (E : RatEllipticCurve) :

The naïve height of an elliptic curve over ℚ.

Equations

E.naiveHeight = 4 * E.A.natAbs ^ 3 ⊔ 27 * E.B.natAbs ^ 2

Instances For

def EllipticCurveRank.RatEllipticCurve.heightLE (H : ℕ) :

Set RatEllipticCurve

The set of elliptic curves over ℚ with naïve height less than or equal to a given height.

Equations

EllipticCurveRank.RatEllipticCurve.heightLE H = {E : EllipticCurveRank.RatEllipticCurve | E.naiveHeight ≤ H}

Instances For

theorem EllipticCurveRank.RatEllipticCurve.card_heightLE_div_pow_five_div_six_tensto :

Filter.Tendsto (fun (H : ℕ) => ↑(heightLE H).ncard / ↑H ^ (5 / 6)) Filter.atTop (nhds (2 ^ (4 / 3) * 3 ^ (-3 / 2) / (riemannZeta 10).re))

Formula (5.1.1) of [PPVW2016]: The number of elliptic curves over ℚ with naïve height at most H is asymptotically 2^(4/3)*3^(-3/2)/ζ(10) * H^(5/6).

theorem EllipticCurveRank.RatEllipticCurve.half_rank_zero_and_half_rank_one (r : ℕ) (hr : r = 0 ∨ r = 1) :

Filter.Tendsto (fun (H : ℕ) => ↑{E : RatEllipticCurve | E ∈ heightLE H ∧ E.rank = r}.ncard / ↑(heightLE H).ncard) Filter.atTop (nhds (1 / 2))

Conjecture by Goldfeld and Katz–Sarnak: if elliptic curves over ℚ are ordered by their heights, then 50% of the curves have rank 0 and 50% have rank 1. See p. 28 of https://people.maths.bris.ac.uk/~matyd/BSD2011/bsd2011-Bhargava.pdf.

theorem EllipticCurveRank.RatEllipticCurve.avg_rank_lt_0885 :

Filter.limsup (fun (H : ℕ) => ↑(∑ᶠ (E : ↑(heightLE H)), (↑E).rank) / ↑(heightLE H).ncard) Filter.atTop < 0.885

Theorem 3 of [BS2013]: when elliptic curves over ℚ are ordered by height, their average rank is < .885.

theorem EllipticCurveRank.RatEllipticCurve.unbounded_rank_conjecture (n : ℕ) :

∃ (E : RatEllipticCurve), n ≤ E.rank

From [PPVW2016], Section 3.1: "from the mid-1960s to the present, it seems that most experts conjectured unboundedness."

theorem EllipticCurveRank.RatEllipticCurve.finite_twentyone_lt_finrank :

{E : RatEllipticCurve | 21 < E.rank}.Finite

From [PPVW2016], Section 8.2: "Our heuristic predicts (a) All but finitely many E ∈ ℰ satisfy rk E(ℚ) ≤ 21". In other words, there are only finitely many elliptic curves over ℚ (up to isomorphism) with rank greater than 21. Notice that this contradicts the previous conjecture.

theorem EllipticCurveRank.RatEllipticCurve.rank_height_count_asymptotic (r : ℕ) (h₁ : 1 ≤ r) (h₂ : r ≤ 20) :

∃ (f : ℕ → ℝ), Filter.Tendsto f Filter.atTop (nhds 0) ∧ ∀ (H : ℕ), 1 < H → ↑{E : RatEllipticCurve | E ∈ heightLE H ∧ r ≤ E.rank}.ncard = ↑H ^ ((21 - ↑r) / 24 + f H)

[PPVW2016] 8.2(b): for 1 ≤ r ≤ 20, the number of elliptic curves over ℚ with rank r and naïve height at most H is asymptotically H ^ ((21 - r) / 24 + o(1)). Note: ℰ_H in 8.2(b) should be ℰ_{≤H}, see the statement of Theorem 7.3.3. When r = 1, the exponent is 20 / 24 = 5 / 6, which agrees with the exponent in card_heightLE_div_pow_five_div_six_tensto and is consistent with half_rank_zero_and_half_rank_one.

theorem EllipticCurveRank.RatEllipticCurve.twentyone_le_rank_height_count_asymptotic :

∃ (f : ℕ → ℝ), Filter.Tendsto f Filter.atTop (nhds 0) ∧ ∀ (H : ℕ), 1 < H → ↑{E : RatEllipticCurve | E ∈ heightLE H ∧ 21 ≤ E.rank}.ncard ≤ ↑H ^ f H

[PPVW2016] 8.2(c): the number of elliptic curves over ℚ with rank ≥ 21 and naïve height at most H is asymptotically at most H ^ o(1).

See https://en.wikipedia.org/wiki/Rank_of_an_elliptic_curve#Largest_known_ranks

def EllipticCurveRank.WeierstrassCurve.elkiesKlagsbrun29 :

WeierstrassCurve ℚ

The elliptic curve over ℚ of rank at least 29 found by Elkies and Klagsbrun in 2024. It has rank exactly 29 assuming the generalized Riemann hypothesis.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem EllipticCurveRank.WeierstrassCurve.Δ_elkiesKlagsbrun29 :

elkiesKlagsbrun29.Δ = -2 ^ 19 * 3 ^ 7 * 5 ^ 7 * 7 ^ 4 * 11 ^ 5 * 13 ^ 3 * 17 ^ 4 * 31 ^ 3 * 41 ^ 2 * 43 ^ 2 * 61 ^ 2 * 233 * 241 ^ 2 * 4139 * 678146849364709860535420504397393 * 159788990966780131363155786084695062643236502969 * 4402149008473369392540402625019227412319473055901

See https://mathoverflow.net/a/478050.

instance EllipticCurveRank.WeierstrassCurve.instIsEllipticRatElkiesKlagsbrun29 :

elkiesKlagsbrun29.IsElliptic

theorem EllipticCurveRank.WeierstrassCurve.twentynine_le_rank_elkiesKlagsbrun29 :

29 ≤ Module.finrank ℤ (WeierstrassCurve.Affine.Point (elkiesKlagsbrun29.baseChange ℚ))

theorem EllipticCurveRank.WeierstrassCurve.rank_elkiesKlagsbrun29 :

Module.finrank ℤ (WeierstrassCurve.Affine.Point (elkiesKlagsbrun29.baseChange ℚ)) = 29

def EllipticCurveRank.WeierstrassCurve.elkies28 :

WeierstrassCurve ℚ

The elliptic curve over ℚ of rank at least 28 found by Elkies in 2006. It has rank exactly 28 assuming the generalized Riemann hypothesis.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem EllipticCurveRank.WeierstrassCurve.Δ_elkies28 :

elkies28.Δ = 2 ^ 15 * 3 ^ 6 * 5 ^ 6 * 7 ^ 4 * 11 ^ 2 * 13 ^ 4 * 17 ^ 5 * 19 ^ 3 * 48463 * 20650099 * 315574902691581877528345013999136728634663121 * 376018840263193489397987439236873583997122096511452343225772113000611087671413

See https://mathoverflow.net/a/478050.

instance EllipticCurveRank.WeierstrassCurve.instIsEllipticRatElkies28 :

elkies28.IsElliptic

theorem EllipticCurveRank.WeierstrassCurve.twentyeight_le_rank_elkies28 :

28 ≤ Module.finrank ℤ (WeierstrassCurve.Affine.Point (elkies28.baseChange ℚ))

theorem EllipticCurveRank.WeierstrassCurve.rank_elkies28 :

Module.finrank ℤ (WeierstrassCurve.Affine.Point (elkies28.baseChange ℚ)) = 28