2607.20408v1 / Repro/ExtremeValues.lean
all files
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.NumberTheory.LSeries.DirichletContinuation
import Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
import Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-!
# Extreme values of quadratic Dirichlet L-functions: formal core
This file fixes the formal meaning of the asymptotic assertion in Theorem 1.1 of
arXiv:2607.20408v1 and proves the order-theoretic (resonance-to-maximum) part of the
argument. The missing analytic estimate is deliberately exposed as a proposition,
not hidden behind a postulate or proof placeholder.
-/
open Filter
open scoped Topology
namespace ExtremeValues
/-- The usual elementary characterization of a fundamental discriminant. -/
def IsFundamentalDiscriminant (d : ℤ) : Prop :=
(d % 4 = 1 ∧ Squarefree d.natAbs) ∨
(∃ m : ℤ, d = 4 * m ∧ (m % 4 = 2 ∨ m % 4 = 3) ∧ Squarefree m.natAbs)
lemma IsFundamentalDiscriminant.ne_zero {d : ℤ} (hd : IsFundamentalDiscriminant d) : d ≠ 0 := by
rintro rfl
rcases hd with h | ⟨m, hm, hmod, -⟩
· norm_num at h
· have : m = 0 := by omega
subst m
norm_num at hmod
lemma IsFundamentalDiscriminant.natAbs_pos {d : ℤ} (hd : IsFundamentalDiscriminant d) :
0 < d.natAbs :=
Int.natAbs_pos.mpr hd.ne_zero
/-- Every positive squarefree integer congruent to `1 mod 4` is a fundamental discriminant. -/
lemma fundamental_of_squarefree_mod_four {d : ℕ} (hsq : Squarefree d) (hmod : d % 4 = 1) :
IsFundamentalDiscriminant d := by
left
constructor
· exact_mod_cast hmod
· simpa using hsq
/-- Iterated natural logarithms, with the same convention as the paper. -/
noncomputable def log2 (x : ℝ) : ℝ := Real.log (Real.log x)
/-- The third iterated natural logarithm. -/
noncomputable def log3 (x : ℝ) : ℝ := Real.log (log2 x)
/-- The scale occurring in Theorem 1.1. -/
noncomputable def extremeScale (x : ℝ) : ℝ :=
Real.sqrt (Real.log x * log3 x / log2 x)
/--
The precise epsilon-form meaning of
`A(X) ≥ exp ((1 + o(1)) * extremeScale X)` used in this development.
Writing the claim this way avoids treating the informal `o(1)` as data. It says
that every constant strictly below `1` is eventually admissible.
-/
def HasExtremeLowerBound (A : ℕ → ℝ) : Prop :=
∀ c : ℝ, c < 1 →
∀ᶠ X : ℕ in atTop, Real.exp (c * extremeScale X) ≤ A X
/-- A finite family of nonnegative resonance weights. -/
structure ResonanceWitness (value : ℤ → ℝ) (X : ℕ) (target : ℝ) where
support : Finset ℤ
weight : ℤ → ℝ
fundamental : ∀ d ∈ support, IsFundamentalDiscriminant d
in_shell : ∀ d ∈ support, X < d.natAbs ∧ d.natAbs ≤ 2 * X
weight_nonneg : ∀ d ∈ support, 0 ≤ weight d
mass_pos : 0 < ∑ d ∈ support, weight d
moment_lower :
target * (∑ d ∈ support, weight d) ≤
∑ d ∈ support, weight d * value d
/--
The completely formal weighted-average step behind equation (3.1): if the weighted
first moment is at least `target` times the mass, one member of the support has value
at least `target`.
-/
theorem ResonanceWitness.exists_value_ge
{value : ℤ → ℝ} {X : ℕ} {target : ℝ}
(R : ResonanceWitness value X target) :
∃ d : ℤ, IsFundamentalDiscriminant d ∧
X < d.natAbs ∧ d.natAbs ≤ 2 * X ∧ target ≤ value d := by
by_contra! h
have hle : ∀ d ∈ R.support, R.weight d * value d ≤ R.weight d * target := by
intro d hd
exact mul_le_mul_of_nonneg_left (le_of_lt (h d (R.fundamental d hd)
(R.in_shell d hd).1 (R.in_shell d hd).2)) (R.weight_nonneg d hd)
have hsum :
(∑ d ∈ R.support, R.weight d * value d) ≤
target * (∑ d ∈ R.support, R.weight d) := by
calc
(∑ d ∈ R.support, R.weight d * value d)
≤ ∑ d ∈ R.support, R.weight d * target := by
exact Finset.sum_le_sum fun d hd ↦ hle d hd
_ = target * (∑ d ∈ R.support, R.weight d) := by
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro d _
ring
have heq :
(∑ d ∈ R.support, R.weight d * value d) =
target * (∑ d ∈ R.support, R.weight d) :=
le_antisymm hsum R.moment_lower
obtain ⟨d, hd, hwd⟩ : ∃ d ∈ R.support, 0 < R.weight d := by
by_contra! hn
have hz : ∀ d ∈ R.support, R.weight d = 0 := by
intro d hd
exact le_antisymm (hn d hd) (R.weight_nonneg d hd)
have : (∑ d ∈ R.support, R.weight d) = 0 := by
exact Finset.sum_eq_zero fun d hd ↦ hz d hd
linarith [R.mass_pos]
have hstrict : R.weight d * value d < R.weight d * target :=
mul_lt_mul_of_pos_left
(h d (R.fundamental d hd) (R.in_shell d hd).1 (R.in_shell d hd).2) hwd
have :
(∑ d ∈ R.support, R.weight d * value d) <
∑ d ∈ R.support, R.weight d * target := by
exact Finset.sum_lt_sum hle ⟨d, hd, hstrict⟩
rw [Finset.mul_sum] at heq
simp_rw [mul_comm target] at heq
exact (ne_of_lt this) heq
/--
An explicit interface for the one genuinely analytic output required from the
resonance calculation. It does not assert the theorem directly: it provides the
finite resonator and its first-moment inequality.
-/
def HasResonanceMoments (value : ℤ → ℝ) : Prop :=
∀ c : ℝ, c < 1 →
∀ᶠ X : ℕ in atTop,
Nonempty (ResonanceWitness value X (Real.exp (c * extremeScale X)))
/-- The shell maximum, written as a supremum so it is defined even for an empty shell. -/
noncomputable def shellSup (value : ℤ → ℝ) (X : ℕ) : ℝ :=
sSup (value '' {d : ℤ | IsFundamentalDiscriminant d ∧
X < d.natAbs ∧ d.natAbs ≤ 2 * X})
/--
The resonance moment inequalities imply the exact epsilon-form of the paper's
extreme-value conclusion.
-/
theorem extreme_lower_bound_of_resonance
{value : ℤ → ℝ} (hres : HasResonanceMoments value) :
HasExtremeLowerBound (shellSup value) := by
intro c hc
filter_upwards [hres c hc] with X hX
let R := Classical.choice hX
obtain ⟨d, hd, hlow, hupp, hvalue⟩ := R.exists_value_ge
apply hvalue.trans
apply le_csSup
· refine Set.Finite.bddAbove ?_
apply Set.Finite.image
apply Set.Finite.subset (Set.finite_Icc (α := ℤ) (-Int.ofNat (2 * X)) (Int.ofNat (2 * X)))
intro z hz
simp only [Set.mem_Icc]
have hzabs := hz.2.2
have hupper : z ≤ (2 * X : ℕ) :=
Int.le_natAbs.trans (by exact_mod_cast hzabs)
have hlower : -z ≤ (2 * X : ℕ) := by
have hnegabs : (-z).natAbs ≤ 2 * X := by simpa using hzabs
exact (Int.le_natAbs (a := -z)).trans (by exact_mod_cast hnegabs)
constructor
· simpa using neg_le_neg hlower
· simpa using hupper
· exact ⟨d, ⟨hd, hlow, hupp⟩, rfl⟩
end ExtremeValues