PrimeSum

formal source

  57
  58/-- The prime sum P(σ) = ∑_p p^{−σ} for real σ.
  59    Converges for σ > 1. -/
  60noncomputable def PrimeSum (σ : ℝ) : ℝ :=
  61  ∑' (p : Nat.Primes), (p : ℝ) ^ (-σ)
  62
  63/-- The Hilbert–Schmidt norm squared of the prime operator A(s):
  64    ‖A(s)‖₂² = ∑_p |p^{−s}|² = ∑_p p^{−2σ}.
  65    This is the key convergence condition. -/
  66noncomputable def HilbertSchmidtNormSq (σ : ℝ) : ℝ :=
  67  ∑' (p : Nat.Primes), (p : ℝ) ^ (-2 * σ)
  68
  69/-- The HS norm converges for σ > 1/2.
  70    Proof: ∑_p p^{−2σ} ≤ ∑_{n≥2} n^{−2σ} ≤ ζ(2σ) − 1 < ∞
  71    since 2σ > 1. -/
  72theorem hilbert_schmidt_convergent {σ : ℝ} (hσ : 1/2 < σ) :
  73    Summable (fun (p : Nat.Primes) => (p : ℝ) ^ (-2 * σ)) := by
  74  exact (Nat.Primes.summable_rpow).2 (by linarith)
  75
  76/-- Each eigenvalue p^{−s} has modulus < 1 for σ > 0.
  77    This ensures each factor (1 − p^{−s}) is nonzero. -/
  78theorem eigenvalue_lt_one {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
  79    (p : ℝ) ^ (-σ) < 1 := by
  80  have hp_one : (1 : ℝ) < p := by
  81    exact_mod_cast p.prop.one_lt
  82  exact Real.rpow_lt_one_of_one_lt_of_neg hp_one (by linarith)
  83
  84/-- Each eigenvalue p^{−s} is positive for σ > 0. -/
  85theorem eigenvalue_pos {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
  86    0 < (p : ℝ) ^ (-σ) := by
  87  exact Real.rpow_pos_of_pos (by exact_mod_cast p.prop.pos) _
  88
  89/-! ### §2. The regularized Fredholm determinant -/
  90