-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The L-series of the twist of the von Mangoldt function `Λ` by a Dirichlet character `χ` at `s`
equals the negative logarithmic derivative of the L-series of `χ` when `re s > 1`. -/
lemma LSeries_twist_vonMangoldt_eq {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
    L (↗χ * ↗Λ) s = - deriv (L ↗χ) s / L ↗χ s

Proof state:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n => χ ↑n) s
hs' : (abscissaOfAbsConv fun n => χ ↑n) < ↑s.re
hΛ : LSeriesSummable ((fun n => χ ↑n) * fun n => ↑(Λ n)) s
⊢ L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s

Tactic:
rw [eq_div_iff <| LSeries_ne_zero_of_one_lt_re χ hs, ← LSeries_convolution' hΛ hχ,
  convolution_twist_vonMangoldt, LSeries_deriv hs', neg_neg]

Result:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n => χ ↑n) s
hs' : (abscissaOfAbsConv fun n => χ ↑n) < ↑s.re
hΛ : LSeriesSummable ((fun n => χ ↑n) * fun n => ↑(Λ n)) s
⊢ L ((fun n => χ ↑n) * fun n => Complex.log ↑n) s = L (logMul fun n => χ ↑n) s

Proof state:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
⊢ L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s

Tactic:
have hχ : LSeriesSummable ↗χ s := (LSeriesSummable_iff hN χ).mpr hs

Result:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n => χ ↑n) s
⊢ L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s

Proof state:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n => χ ↑n) s
hs' : (abscissaOfAbsConv fun n => χ ↑n) < ↑s.re
⊢ L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s

Tactic:
have hΛ : LSeriesSummable (↗χ * ↗Λ) s := LSeriesSummable_twist_vonMangoldt χ hs

Result:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n => χ ↑n) s
hs' : (abscissaOfAbsConv fun n => χ ↑n) < ↑s.re
hΛ : LSeriesSummable ((fun n => χ ↑n) * fun n => ↑(Λ n)) s
⊢ L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s

Proof state:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n => χ ↑n) s
hs' : (abscissaOfAbsConv fun n => χ ↑n) < ↑s.re
hΛ : LSeriesSummable ((fun n => χ ↑n) * fun n => ↑(Λ n)) s
⊢ L ((fun n => χ ↑n) * fun n => Complex.log ↑n) s = L (logMul fun n => χ ↑n) s

Tactic:
exact LSeries_congr s fun _ ↦ by simp [mul_comm, logMul]

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n => χ ↑n) s
hs' : (abscissaOfAbsConv fun n => χ ↑n) < ↑s.re
hΛ : LSeriesSummable ((fun n => χ ↑n) * fun n => ↑(Λ n)) s
n✝ : ℕ
x✝ : n✝ ≠ 0
⊢ ((fun n => χ ↑n) * fun n => Complex.log ↑n) n✝ = logMul (fun n => χ ↑n) n✝

Tactic:
simp [mul_comm, logMul]

Result:
no goals

Proof state:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n => χ ↑n) s
⊢ L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s

Tactic:
have hs' : abscissaOfAbsConv ↗χ < s.re := by
  rwa [absicssaOfAbsConv_eq_one hN, ← EReal.coe_one, EReal.coe_lt_coe_iff]

Result:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n => χ ↑n) s
hs' : (abscissaOfAbsConv fun n => χ ↑n) < ↑s.re
⊢ L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s

Tactic:
rcases eq_or_ne N 0 with rfl | hN

Result:
case inl
s : ℂ
hs : 1 < s.re
χ : DirichletCharacter ℂ 0
⊢ L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s

case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
⊢ L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n => χ ↑n) s
⊢ (abscissaOfAbsConv fun n => χ ↑n) < ↑s.re

Tactic:
rwa [absicssaOfAbsConv_eq_one hN, ← EReal.coe_one, EReal.coe_lt_coe_iff]

Result:
no goals

Proof state:
case inl
s : ℂ
hs : 1 < s.re
χ : DirichletCharacter ℂ 0
⊢ L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s

Tactic:
simpa [-deriv_const', modZero_eq_delta, delta_mul_eq_smul_delta, LSeries_delta]
  using deriv_const s (1 : ℂ)

Result:
no goals