Source indexedlemma · leanprover/lean4:v4.32.0

DerivZeta0EqDerivZeta

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1423 to 1433

Mathematical statement

Exact Lean statement

lemma DerivZeta0EqDerivZeta {N : ℕ} (N_pos : 0 < N) {s : ℂ} (reS_pos : 0 < s.re)
    (s_ne_one : s ≠ 1) :
    deriv (ζ₀ N) s = ζ' s

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma DerivZeta0EqDerivZeta {N : ℕ} (N_pos : 0 < N) {s : ℂ} (reS_pos : 0 < s.re)    (s_ne_one : s ≠ 1) :    deriv (ζ₀ N) s = ζ' s := by  let U := {z : ℂ | z ≠ 1 ∧ 0 < z.re}  have {x : ℂ} (hx : x ∈ U) : ζ₀ N x = ζ x := by    simp only [mem_setOf_eq, U] at hx; exact Zeta0EqZeta (N := N) N_pos hx.2 hx.1  refine deriv_eqOn isOpen_aux ?_ (by simp [s_ne_one, reS_pos])  intro x hx  have hζ := HolomorphicOn_riemannZeta.mono (by aesop)|>.hasDerivAt (s := U) <|    isOpen_aux.mem_nhds hx  exact hζ.hasDerivWithinAt.congr (fun y hy ↦ this hy) (this hx)