Theorem: DirichletCharacter.LSeries_eulerProduct' (EulerProducts/PNT.lean)

State before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -(1 - χ ↑↑p * ↑↑p ^ (-s)).log) = L (fun n => χ ↑n) s
Tactic:
rw [LSeries]
State after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -(1 - χ ↑↑p * ↑↑p ^ (-s)).log) = ∑' (n : ℕ), term (fun n => χ ↑n) s n

State before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -(1 - χ ↑↑p * ↑↑p ^ (-s)).log) = ∑' (n : ℕ), term (fun n => χ ↑n) s n
Tactic:
convert exp_sum_primes_log_eq_tsum (f := dirichletSummandHom χ <| ne_zero_of_one_lt_re hs) <|
  summable_dirichletSummand χ hs
State after:
case h.e'_3.h.e'_5.h.h.e
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ : ℕ
⊢ term (fun n => χ ↑n) s = ⇑(dirichletSummandHom χ ⋯)

State before:
case h.e'_3.h.e'_5.h.h.e
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ : ℕ
⊢ term (fun n => χ ↑n) s = ⇑(dirichletSummandHom χ ⋯)
Tactic:
ext n
State after:
case h.e'_3.h.e'_5.h.h.e.h
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ n : ℕ
⊢ term (fun n => χ ↑n) s n = (dirichletSummandHom χ ⋯) n

State before:
case h.e'_3.h.e'_5.h.h.e.h
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ n : ℕ
⊢ term (fun n => χ ↑n) s n = (dirichletSummandHom χ ⋯) n
Tactic:
rcases eq_or_ne n 0 with rfl | hn
State after:
case h.e'_3.h.e'_5.h.h.e.h.inl
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ : ℕ
⊢ term (fun n => χ ↑n) s 0 = (dirichletSummandHom χ ⋯) 0

case h.e'_3.h.e'_5.h.h.e.h.inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ n : ℕ
hn : n ≠ 0
⊢ term (fun n => χ ↑n) s n = (dirichletSummandHom χ ⋯) n

State before:
case h.e'_3.h.e'_5.h.h.e.h.inl
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ : ℕ
⊢ term (fun n => χ ↑n) s 0 = (dirichletSummandHom χ ⋯) 0
Tactic:
simp only [term_zero, map_zero]
State after:
no goals

State before:
case h.e'_3.h.e'_5.h.h.e.h.inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ n : ℕ
hn : n ≠ 0
⊢ term (fun n => χ ↑n) s n = (dirichletSummandHom χ ⋯) n
Tactic:
simp [hn, dirichletSummandHom, div_eq_mul_inv, cpow_neg]
State after:
no goals