sato_tate_abelian_surfaces
Disprovedabelianvarietiesalgebraalgebraic-geometryl-functionsnumbertheoryopenproblemproved
Sato-Tate conjecture for abelian surfaces: The distribution of normalized Frobenius traces for a genus-2 curve follows one of 55 possible distributions depending on the endomorphism algebra. Proved for elliptic curves (Taylor et al. 2011); abelian surfaces are largely open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem sato_tate_abelian_surfaces (A B : ℤ) (C D : ℤ) :
∃ (density : ℝ → ℝ),
∀ alpha beta : ℝ, alpha ≤ beta →
Filter.Tendsto (fun x : ℝ =>
(∑ p ∈ (Finset.range (Nat.floor x)).filter Nat.Prime,
if alpha ≤ (A + B : ℝ) / (2 * Real.sqrt p) ∧
(A + B : ℝ) / (2 * Real.sqrt p) ≤ beta
then (1 : ℝ) else 0) /
(Nat.primeCounting (Nat.floor x) : ℝ))
Filter.atTop (nhds (∫ t in alpha..beta, density t)) := by
sorrySource