Theorem: summable_neg_log_one_sub_char_mul_prime_cpow (EulerProducts/PNT.lean)

State before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ Summable fun p => -(1 - χ ↑↑p * ↑↑p ^ (-s)).log
Tactic:
have (p : Nat.Primes) : ‖χ p * (p : ℂ) ^ (-s)‖ ≤ (p : ℝ) ^ (-s).re := by
  rw [norm_mul, norm_natCast_cpow_of_re_ne_zero _ <| re_neg_ne_zero_of_one_lt_re hs]
  calc ‖χ p‖ * (p : ℝ) ^ (-s).re
    _ ≤ 1 * (p : ℝ) ^ (-s.re) := by gcongr; exact DirichletCharacter.norm_le_one χ _
    _ = _ := one_mul _
State after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ Summable fun p => -(1 - χ ↑↑p * ↑↑p ^ (-s)).log

State before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ Summable fun p => -(1 - χ ↑↑p * ↑↑p ^ (-s)).log
Tactic:
refine (Nat.Primes.summable_rpow.mpr ?_).of_nonneg_of_le (fun _ ↦ norm_nonneg _) this
  |>.of_norm.neg_clog_one_sub
State after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ (-s).re < -1

State before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ (-s).re < -1
Tactic:
simp only [neg_re, neg_lt_neg_iff, hs]
State after:
no goals

State before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
Tactic:
rw [norm_mul, norm_natCast_cpow_of_re_ne_zero _ <| re_neg_ne_zero_of_one_lt_re hs]
State after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖χ ↑↑p‖ * ↑↑p ^ (-s).re ≤ ↑↑p ^ (-s).re

State before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖χ ↑↑p‖ * ↑↑p ^ (-s).re ≤ ↑↑p ^ (-s).re
Tactic:
calc ‖χ p‖ * (p : ℝ) ^ (-s).re
  _ ≤ 1 * (p : ℝ) ^ (-s.re) := by gcongr; exact DirichletCharacter.norm_le_one χ _
  _ = _ := one_mul _
State after:
no goals

State before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖χ ↑↑p‖ * ↑↑p ^ (-s).re ≤ 1 * ↑↑p ^ (-s.re)
Tactic:
gcongr
State after:
case h
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖χ ↑↑p‖ ≤ 1

State before:
case h
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖χ ↑↑p‖ ≤ 1
Tactic:
exact DirichletCharacter.norm_le_one χ _
State after:
no goals