carrierLog

formal source

 181
 182/-- The log of the carrier: log C(σ) = 2∑_p [log(1−p^{−σ}) + p^{−σ}].
 183    Equivalently: log C(σ) = −2∑_{m≥2} P(mσ)/m. -/
 184noncomputable def carrierLog (σ : ℝ) : ℝ :=
 185  2 * ∑' (p : Nat.Primes), det2LogFactor p σ
 186
 187/-- The carrier value: C(σ) = exp(log C(σ)).
 188    This represents C(s) = ∏_p (1−p^{−s})² exp(2p^{−s}). -/
 189noncomputable def carrierValue (σ : ℝ) : ℝ :=
 190  Real.exp (carrierLog σ)
 191
 192/-- The carrier log-series converges on Re(s) > 1/2. -/
 193theorem carrier_log_convergent {σ : ℝ} (hσ : 1/2 < σ) :
 194    Summable (fun (p : Nat.Primes) => det2LogFactor p σ) :=
 195  det2_product_convergent hσ
 196
 197/-- The carrier is positive (hence nonzero) for real σ > 1/2. -/
 198theorem carrier_pos {σ : ℝ} (hσ : 1/2 < σ) :
 199    0 < carrierValue σ := by
 200  unfold carrierValue
 201  exact Real.exp_pos _
 202
 203/-- The carrier is nonvanishing on Re(s) > 1/2.
 204    Proof: C(s) = exp(log C(s)), and exp is never zero.
 205    The log converges by det2_log_summable. -/
 206theorem carrier_nonvanishing {σ : ℝ} (hσ : 1/2 < σ) :
 207    carrierValue σ ≠ 0 :=
 208  ne_of_gt (carrier_pos hσ)
 209
 210/-! ### §4. Logarithmic derivative bound -/
 211
 212/-- The per-prime contribution to the logarithmic derivative:
 213    d/dσ [log det₂_factor] = p^{−2σ}·(log p)/(1 − p^{−σ}).
 214    (On the real axis; for complex s, use |·|.) -/