Extreme values of quadratic Dirichlet L-functions
In this paper, we investigate extreme values of quadratic Dirichlet L-functions at the central point. We provide new extreme values of L(\frac12,χ_d) as d is large, which improves the recent result of Darbar and Maiti.
The paper claims, under GRH, that the maximum of |L(1/2, \chi_d)| over X < |d| ≤ 2X is at least \exp((1+o(1))\sqrt{\log X \log_3 X / \log_2 X}) — improving the leading constant in the known lower bound to 1 for a fundamental family of L-functions.
Reproduction
~ partially reproduced
Attempted: Lean proves the epsilon-form extreme-value bound for the positive odd fundamental-discriminant subfamily, assuming GRHForPositiveOddQuadratic and GRHImpliesPaperResonanceMoments — the latter being the paper's still-unformalized analytic core, not an accepted external theorem, which is why this is partial rather than conditional. The Jacobi-character semantics and the resonance-moment-to-maximum argument are proved outright.
All modules compile with zero proof placeholders and no project axioms. The missing work: the parity-correct approximate functional equation and error bounds, the GRH quadratic-character mean estimate, and the sharp squarefree GCD-sum construction. Two errors in the paper's printed formulas were found and machine-verified: Lemma 2.1 uses the even gamma factor for negative discriminants, with d = −4 as a concrete failing case, and the Euler product for g₂ has a minus where a plus is required. Both look repairable and neither refutes the main theorem; exact locations and the verification are in the run's README. Independent re-verification: all modules elaborate cleanly, kernel-checked.
trace (164 events) · code (8 files)