theorem
proved
term proof
carrier_nonvanishing
show as:
view Lean formalization →
formal statement (Lean)
206theorem carrier_nonvanishing {σ : ℝ} (hσ : 1/2 < σ) :
207 carrierValue σ ≠ 0 :=
proof body
Term-mode proof.
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 |·|.) -/