Theorem: LogDerivativeDirichlet (PrimeNumberTheoremAnd/MediumPNT.lean)

State before:
s : ℂ
hs : 1 < s.re
⊢ -deriv riemannZeta s / riemannZeta s = ∑' (n : ℕ), ↑(Λ n) / ↑n ^ s
Tactic:
rw [← ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs]
State after:
s : ℂ
hs : 1 < s.re
⊢ LSeries (fun n => ↑(Λ n)) s = ∑' (n : ℕ), ↑(Λ n) / ↑n ^ s

State before:
s : ℂ
hs : 1 < s.re
⊢ LSeries (fun n => ↑(Λ n)) s = ∑' (n : ℕ), ↑(Λ n) / ↑n ^ s
Tactic:
dsimp [LSeries, LSeries.term]
State after:
s : ℂ
hs : 1 < s.re
⊢ (∑' (n : ℕ), if n = 0 then 0 else ↑(Λ n) / ↑n ^ s) = ∑' (n : ℕ), ↑(Λ n) / ↑n ^ s

State before:
s : ℂ
hs : 1 < s.re
⊢ (∑' (n : ℕ), if n = 0 then 0 else ↑(Λ n) / ↑n ^ s) = ∑' (n : ℕ), ↑(Λ n) / ↑n ^ s
Tactic:
nth_rewrite 2 [tsum_eq_add_tsum_ite (b := 0) ?_]
State after:
s : ℂ
hs : 1 < s.re
⊢ (∑' (n : ℕ), if n = 0 then 0 else ↑(Λ n) / ↑n ^ s) =
    ↑(Λ 0) / ↑0 ^ s + ∑' (n : ℕ), if n = 0 then 0 else ↑(Λ n) / ↑n ^ s

s : ℂ
hs : 1 < s.re
⊢ Summable fun n => ↑(Λ n) / ↑n ^ s

State before:
s : ℂ
hs : 1 < s.re
⊢ (∑' (n : ℕ), if n = 0 then 0 else ↑(Λ n) / ↑n ^ s) =
    ↑(Λ 0) / ↑0 ^ s + ∑' (n : ℕ), if n = 0 then 0 else ↑(Λ n) / ↑n ^ s
Tactic:
simp
State after:
no goals

State before:
s : ℂ
hs : 1 < s.re
⊢ Summable fun n => ↑(Λ n) / ↑n ^ s
Tactic:
have := ArithmeticFunction.LSeriesSummable_vonMangoldt hs
State after:
s : ℂ
hs : 1 < s.re
this : LSeriesSummable (fun n => ↑(Λ n)) s
⊢ Summable fun n => ↑(Λ n) / ↑n ^ s

State before:
s : ℂ
hs : 1 < s.re
this : LSeriesSummable (fun n => ↑(Λ n)) s
⊢ Summable fun n => ↑(Λ n) / ↑n ^ s
Tactic:
dsimp [LSeriesSummable] at this
State after:
s : ℂ
hs : 1 < s.re
this : Summable (LSeries.term (fun n => ↑(Λ n)) s)
⊢ Summable fun n => ↑(Λ n) / ↑n ^ s

State before:
s : ℂ
hs : 1 < s.re
this : Summable (LSeries.term (fun n => ↑(Λ n)) s)
⊢ Summable fun n => ↑(Λ n) / ↑n ^ s
Tactic:
convert this
State after:
case h.e'_5.h
s : ℂ
hs : 1 < s.re
this : Summable (LSeries.term (fun n => ↑(Λ n)) s)
x✝ : ℕ
⊢ ↑(Λ x✝) / ↑x✝ ^ s = LSeries.term (fun n => ↑(Λ n)) s x✝

State before:
case h.e'_5.h
s : ℂ
hs : 1 < s.re
this : Summable (LSeries.term (fun n => ↑(Λ n)) s)
x✝ : ℕ
⊢ ↑(Λ x✝) / ↑x✝ ^ s = LSeries.term (fun n => ↑(Λ n)) s x✝
Tactic:
rename ℕ => n
State after:
case h.e'_5.h
s : ℂ
hs : 1 < s.re
this : Summable (LSeries.term (fun n => ↑(Λ n)) s)
n : ℕ
⊢ ↑(Λ n) / ↑n ^ s = LSeries.term (fun n => ↑(Λ n)) s n

State before:
case h.e'_5.h
s : ℂ
hs : 1 < s.re
this : Summable (LSeries.term (fun n => ↑(Λ n)) s)
n : ℕ
⊢ ↑(Λ n) / ↑n ^ s = LSeries.term (fun n => ↑(Λ n)) s n
Tactic:
by_cases h : n = 0 <;> simp [LSeries.term, h]
State after:
no goals