2607.20408v1 / Repro/CentralClaim.lean

all files

import Repro.ExtremeValues
import Repro.QuadraticCharacters

/-!
# The central claim and the remaining analytic interface

We work with the positive odd fundamental-discriminant subfamily
`q > 1`, `Squarefree q`, `q ≡ 1 (mod 4)`.  Proving the lower bound on this
subfamily is stronger than proving it after maximizing over all fundamental
discriminants, and it avoids the parity error in Lemma 2.1 of the paper.
-/

open Filter
open scoped Topology

namespace ExtremeValues

/-- The positive odd fundamental-discriminant subfamily. -/
def IsPositiveOddFundamental (d : ℤ) : Prop :=
  1 < d ∧ Squarefree d.toNat ∧ d.toNat % 4 = 1

theorem IsPositiveOddFundamental.isFundamental {d : ℤ}
    (hd : IsPositiveOddFundamental d) : IsFundamentalDiscriminant d := by
  rcases hd with ⟨hdgt, hsq, hmod⟩
  have hdnonneg : 0 ≤ d := by omega
  have hdcast : (d.toNat : ℤ) = d := Int.toNat_of_nonneg hdnonneg
  have habs : d.natAbs = d.toNat :=
    Int.ofNat_inj.mp ((Int.natAbs_of_nonneg hdnonneg).trans hdcast.symm)
  left
  constructor
  · rw [← hdcast]
    exact_mod_cast hmod
  · simpa [habs] using hsq

/--
The central norm for the repaired positive odd subfamily, extended by zero away
from that subfamily.  This is an actual mathlib analytic continuation of the
bundled Jacobi-symbol Dirichlet character.
-/
noncomputable def positiveOddCentralNorm (d : ℤ) : ℝ :=
  by
    classical
    exact if hd : IsPositiveOddFundamental d then
      have hdgt : 1 < d := hd.1
      have hdnonneg : 0 ≤ d := by omega
      have hdcast : (d.toNat : ℤ) = d := Int.toNat_of_nonneg hdnonneg
      have hq : 1 < d.toNat := by
        exact_mod_cast (show (1 : ℤ) < (d.toNat : ℤ) by simpa [hdcast] using hd.1)
      ‖jacobiLFunction d.toNat hq (1 / 2)‖
    else 0

theorem positiveOddCentralNorm_of_mem {d : ℤ} (hd : IsPositiveOddFundamental d) :
    positiveOddCentralNorm d =
      ‖jacobiLFunction d.toNat (by
        have hdgt : 1 < d := hd.1
        have hdnonneg : 0 ≤ d := by omega
        have hdcast : (d.toNat : ℤ) = d := Int.toNat_of_nonneg hdnonneg
        exact_mod_cast (show (1 : ℤ) < (d.toNat : ℤ) by simpa [hdcast] using hd.1) :
          1 < d.toNat) (1 / 2)‖ := by
  rw [positiveOddCentralNorm]
  simp only [dif_pos hd]

theorem positiveOddCentralNorm_of_not_mem {d : ℤ} (hd : ¬IsPositiveOddFundamental d) :
    positiveOddCentralNorm d = 0 := by
  rw [positiveOddCentralNorm]
  simp only [dif_neg hd]

/--
GRH for exactly the primitive quadratic family used in the repaired statement.
The definition is explicit: every nontrivial zero has real part `1/2`.
-/
def GRHForPositiveOddQuadratic : Prop :=
  ∀ (q : ℕ) (hq : 1 < q), Squarefree q → q % 4 = 1 →
    ∀ s : ℂ, jacobiLFunction q hq s = 0 →
      s.re = 1 / 2

/--
The analytic theorem still missing from the formalization.  This is the exact
finite-moment output of equations (3.2)--(3.8), not a postulate and not the
extreme-value conclusion itself.
-/
def GRHImpliesPaperResonanceMoments : Prop :=
  GRHForPositiveOddQuadratic → HasResonanceMoments positiveOddCentralNorm

/--
The central extreme-value theorem follows formally from GRH and the paper's
claimed resonance moment estimate.
-/
theorem extreme_values_of_quadratic_dirichlet_L
    (hGRH : GRHForPositiveOddQuadratic)
    (hMoment : GRHImpliesPaperResonanceMoments) :
    HasExtremeLowerBound (shellSup positiveOddCentralNorm) :=
  extreme_lower_bound_of_resonance (hMoment hGRH)

end ExtremeValues