Some conjectures about ranks of elliptic curves over ℚ
[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 ex...
Mathematical statement
[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.
Statement source: Wikipedia statement material
Statement terms: CC-BY-SA-4.0
Attributed source material. Reuse must follow the linked attribution and share-alike terms.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
rank_height_count_asymptotic
theorem rank_height_count_asymptotic (r : ℕ) (h₁ : 1 ≤ r) (h₂ : r ≤ 20) : ∃ f : ℕ → ℝ, atTop.Tendsto f (𝓝 0) ∧ ∀ H : ℕ, 1 < H → {E ∈ heightLE H | r ≤ E.rank}.ncard = (H : ℝ) ^ ((21 - r) / 24 + f H) := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References