awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
n : ℕ
h₁ : ¬Eq (α := ZMod N) (↑n : ZMod N) 1
h_1 : ¬n = 0
⊢ 0 ≤ norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s

Tactic:
LSeriesSummable_of_bounded_of_one_lt_re (fun _ _ ↦ χ.norm_le_one _) hs

Premises used: DirichletCharacter.norm_le_one, LSeriesSummable_of_bounded_of_one_lt_re
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
⊢ LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s ↔ 1 < s.re

Tactic:
⟨fun H ↦ ?_, LSeriesSummable_of_one_lt_re χ⟩

Premises used: DirichletCharacter.LSeriesSummable_of_one_lt_re, Iff.intro
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
refine : ∀ (H : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s), 1 < s.re
⊢ LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s ↔ 1 < s.re

Tactic:
refine ⟨fun H ↦ ?_, LSeriesSummable_of_one_lt_re χ⟩
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
by_contra! : ∀ (h : s.re ≤ 1), False
⊢ 1 < s.re

Tactic:
by_contra! h
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
h : s.re ≤ 1
⊢ s.re ≤ re 1

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
h : s.re ≤ 1
⊢ False

Tactic:
exact not_LSeriesSummable_at_one hN χ <| LSeriesSummable.of_re_le_re (by simp [h]) H

Premises used: DirichletCharacter.not_LSeriesSummable_at_one, LSeriesSummable.of_re_le_re
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hn : N ≠ 0
χ : DirichletCharacter ℂ N
⊢ (abscissaOfAbsConv fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) = 1

Tactic:
simpa [abscissaOfAbsConv, LSeriesSummable_iff hn χ, Set.Ioi_def, EReal.image_coe_Ioi]
    using csInf_Ioo <| EReal.coe_lt_top 1

Premises used: DirichletCharacter.LSeriesSummable_iff, csInf_Ioo, OfNat.ofNat, EReal.image_coe_Ioi, EReal.coe_lt_top, Set.Ioi_def, LSeries.abscissaOfAbsConv
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ LSeriesSummable ((fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) * f) s

Tactic:
.of_norm <| h.norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) fun n ↦ norm_term_le s ?_

Premises used: HMul.hMul, Summable.of_norm, Summable.of_nonneg_of_le, Nat.cast, Summable.norm, LSeries.term, LSeries.norm_term_le, DFunLike.coe, norm_nonneg, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
refine : ∀ (n : ℕ), ‖HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) f n‖ ≤ ‖f n‖
⊢ LSeriesSummable ((fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) * f) s

Tactic:
refine .of_norm <| h.norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) fun n ↦ norm_term_le s ?_

Premises used: Summable.of_nonneg_of_le, Summable.norm, LSeries.norm_term_le, norm_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
n : ℕ
⊢ ‖HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) f n‖ ≤ ‖f n‖

Tactic:
simpa using mul_le_of_le_one_left (norm_nonneg <| f n) <| χ.norm_le_one n

Premises used: DirichletCharacter.norm_le_one, Nat.cast, mul_le_of_le_one_left, norm_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
rw :
  L
      ((fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) ⍟
        HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
          (↑((μ : (a : ℕ) → ℤ) n) : ℂ))
      s =
    1
rw₁ : L δ s = 1
rw₂ : Eq (α := ℂ) (1 s) 1
rw₃ rw₄ : Eq (α := ℂ) 1 1
⊢ L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s *
      L
        (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
          (↑((μ : (a : ℕ) → ℤ) n) : ℂ))
        s =
    1

Tactic:
rw [← LSeries_convolution' (LSeriesSummable_of_one_lt_re χ hs) <|
          LSeriesSummable_mul χ <| ArithmeticFunction.LSeriesSummable_moebius_iff.mpr hs,
    convolution_mul_moebius, LSeries_delta, Pi.one_apply]

Premises used: Iff.mpr, DirichletCharacter.LSeriesSummable_of_one_lt_re, Pi.one_apply, DirichletCharacter.LSeriesSummable_mul, LSeries_convolution', LSeries_delta, ArithmeticFunction.LSeriesSummable_moebius_iff, DirichletCharacter.convolution_mul_moebius
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s = 0
⊢ False

Tactic:
simpa [h] using LSeries.mul_mu_eq_one χ hs

Premises used: DirichletCharacter.LSeries.mul_mu_eq_one
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
⊢ abscissaOfAbsConv 1 = 1

Tactic:
modOne_eq_one (χ := χ₁) ▸ absicssaOfAbsConv_eq_one one_ne_zero χ₁

Premises used: Eq.rec, DirichletCharacter.modOne_eq_one, DirichletCharacter.absicssaOfAbsConv_eq_one, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
⊢ LSeriesSummable 1 s ↔ 1 < s.re

Tactic:
modOne_eq_one (χ := χ₁) ▸ LSeriesSummable_iff one_ne_zero χ₁

Premises used: Eq.rec, DirichletCharacter.modOne_eq_one, DirichletCharacter.LSeriesSummable_iff, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
h : ∀ (s : ℂ), L (fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) s = L 1 s
⊢ (L fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) = L 1

Tactic:
ext s
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
⊢ L (fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) s = L 1 s

Tactic:
(LSeries_congr const_one_eq_zeta s).symm

Premises used: LSeries_congr, Eq.symm, ArithmeticFunction.const_one_eq_zeta
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
⊢ L (fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) s = L 1 s

Tactic:
exact (LSeries_congr const_one_eq_zeta s).symm

Premises used: LSeries_congr, Eq.symm, ArithmeticFunction.const_one_eq_zeta
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
⊢ LSeriesSummable (fun (x : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) x) : ℂ)) s ↔ 1 < s.re

Tactic:
(LSeriesSummable_congr s const_one_eq_zeta).symm.trans <| LSeriesSummable_one_iff

Premises used: LSeriesSummable_congr, LSeriesSummable_one_iff, Iff.trans, Iff.symm, ArithmeticFunction.const_one_eq_zeta
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℂ) (↑((ζ : (a : ℕ) → ℕ) n) : ℂ) (1 n)

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
rw : abscissaOfAbsConv 1 = 1
rw₁ rw₂ : Eq (α := EReal) 1 1
⊢ (abscissaOfAbsConv fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) = 1

Tactic:
rw [abscissaOfAbsConv_congr (g := 1) fun hn ↦ by simp [hn], abscissaOfAbsConv_one]

Premises used: LSeries.abscissaOfAbsConv_one, LSeries.abscissaOfAbsConv_congr
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
this :
  Eq (α := ℂ) (∑' (n : ℕ), term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n)
    (∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s)
⊢ L (fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) s = riemannZeta s

Tactic:
simpa [LSeries, zeta_eq_tsum_one_div_nat_cpow hs]

Premises used: zeta_eq_tsum_one_div_nat_cpow, LSeries
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
suffices :
  Eq (α := ℂ) (∑' (n : ℕ), term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n)
    (∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s)
⊢ L (fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) s = riemannZeta s

Tactic:
suffices ∑' n, term (fun n ↦ if n = 0 then 0 else 1) s n = ∑' n : ℕ, 1 / (n : ℂ) ^ s by
    simpa [LSeries, zeta_eq_tsum_one_div_nat_cpow hs]
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ Eq (α := ℂ) (∑' (n : ℕ), term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n)
    (∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s)

Tactic:
tsum_congr fun n ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
refine : ∀ (n : ℕ), term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n = 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ Eq (α := ℂ) (∑' (n : ℕ), term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n)
    (∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s)

Tactic:
refine tsum_congr fun n ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
n : ℕ
inl : ∀ (hn : n = 0), term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n = 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
inr : ∀ (hn : n ≠ 0), term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n = 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n = 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
rcases eq_or_ne n 0 with hn | hn

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n = 0
⊢ term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n = 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
simp [hn, ne_zero_of_one_lt_re hs]

Premises used: Complex.ne_zero_of_one_lt_re
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n = 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
simp [hn, ne_zero_of_one_lt_re hs]

Premises used: Complex.ne_zero_of_one_lt_re
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ LSeriesHasSum (fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) s (riemannZeta s)

Tactic:
LSeries_zeta_eq_riemannZeta hs ▸ (LSeriesSummable_zeta_iff.mpr hs).LSeriesHasSum

Premises used: Iff.mpr, Eq.rec, LSeriesSummable.LSeriesHasSum, ArithmeticFunction.LSeries_zeta_eq_riemannZeta, ArithmeticFunction.LSeriesSummable_zeta_iff
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
rw : L ((fun (x : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) x) : ℂ)) ⍟ fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) s = 1
⊢ L (fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) s * L (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) s = 1

Tactic:
rw [← LSeries_convolution' (LSeriesSummable_zeta_iff.mpr hs)
    (LSeriesSummable_moebius_iff.mpr hs)]

Premises used: Iff.mpr, LSeries_convolution', ArithmeticFunction.LSeriesSummable_moebius_iff, ArithmeticFunction.LSeriesSummable_zeta_iff
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ L ((fun (x : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) x) : ℂ)) ⍟ fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) s = 1

Tactic:
simp [← natCoe_apply, ← intCoe_apply, coe_mul, one_eq_delta, LSeries_delta, -zeta_apply]

Premises used: ArithmeticFunction.zeta_apply, ArithmeticFunction.coe_mul, ArithmeticFunction.one_eq_delta, LSeries_delta, ArithmeticFunction.natCoe_apply, ArithmeticFunction.intCoe_apply
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
h : L (fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) s = 0
⊢ False

Tactic:
simpa [h, -zeta_apply] using LSeries_zeta_mul_Lseries_moebius hs

Premises used: ArithmeticFunction.zeta_apply, ArithmeticFunction.LSeries_zeta_mul_Lseries_moebius
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ L 1 s = riemannZeta s

Tactic:
LSeries_zeta_eq ▸ LSeries_zeta_eq_riemannZeta hs

Premises used: ArithmeticFunction.LSeries_zeta_eq, Eq.rec, ArithmeticFunction.LSeries_zeta_eq_riemannZeta
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ LSeriesHasSum 1 s (riemannZeta s)

Tactic:
LSeries_one_eq_riemannZeta hs ▸ (LSeriesSummable_one_iff.mpr hs).LSeriesHasSum

Premises used: Iff.mpr, Eq.rec, LSeriesSummable.LSeriesHasSum, LSeries_one_eq_riemannZeta, LSeriesSummable_one_iff
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ L 1 s * L (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) s = 1

Tactic:
LSeries_zeta_eq ▸ LSeries_zeta_mul_Lseries_moebius hs

Premises used: ArithmeticFunction.LSeries_zeta_mul_Lseries_moebius, ArithmeticFunction.LSeries_zeta_eq, Eq.rec
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ L 1 s ≠ 0

Tactic:
LSeries_zeta_eq ▸ LSeries_zeta_ne_zero_of_one_lt_re hs

Premises used: ArithmeticFunction.LSeries_zeta_ne_zero_of_one_lt_re, ArithmeticFunction.LSeries_zeta_eq, Eq.rec
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ riemannZeta s ≠ 0

Tactic:
LSeries_one_eq_riemannZeta hs ▸ LSeries_one_ne_zero_of_one_lt_re hs

Premises used: Eq.rec, LSeries_one_eq_riemannZeta, LSeries_one_ne_zero_of_one_lt_re
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
x : ℝ
hx : 1 < x
⊢ 1 < (↑x : ℂ).re

Tactic:
simpa using hx
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
x : ℝ
hx : 1 < x
⊢ 1 < (↑x : ℂ).re

Tactic:
have hx' : 1 < (x : ℂ).re := by simpa using hx
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
x : ℝ
hx : 1 < x
hx' : 1 < (↑x : ℂ).re
rw : 0 < L 1 (↑x : ℂ)
⊢ 0 < riemannZeta (↑x : ℂ)

Tactic:
rw [← LSeries_one_eq_riemannZeta hx']

Premises used: LSeries_one_eq_riemannZeta
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
x : ℝ
hx : 1 < x
hx' : 1 < (↑x : ℂ).re
x_1 : ℕ
⊢ LE.le (α := (fun (a : ℕ) ↦ ℂ) x_1) (0 x_1) (1 x_1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
x : ℝ
hx : 1 < x
hx' : 1 < (↑x : ℂ).re
⊢ LT.lt (α := ℂ) 0 (1 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
x : ℝ
hx : 1 < x
hx' : 1 < (↑x : ℂ).re
refine : abscissaOfAbsConv 1 < (↑x : EReal)
⊢ 0 < L 1 (↑x : ℂ)

Tactic:
refine LSeries.positive (fun _ ↦ by simp) (by simp) ?_

Premises used: LSeries.positive
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
x : ℝ
hx : 1 < x
hx' : 1 < (↑x : ℂ).re
⊢ 1 < (↑x : EReal)

Tactic:
exact_mod_cast hx
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
x : ℝ
hx : 1 < x
hx' : 1 < (↑x : ℂ).re
simpa : 1 < (↑x : EReal)
⊢ abscissaOfAbsConv 1 < (↑x : EReal)

Tactic:
simpa [LSeries.abscissaOfAbsConv_one] using (by exact_mod_cast hx : (1 : EReal) < x)

Premises used: LSeries.abscissaOfAbsConv_one
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
x : ℝ
hx : 1 < x
⊢ 0 < (riemannZeta (↑x : ℂ)).re

Tactic:
(Complex.pos_iff.mp (riemannZeta_pos_of_one_lt hx)).1

Premises used: riemannZeta_pos_of_one_lt, And.left, Complex.pos_iff, Iff.mp
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
x : ℝ
hx : 1 < x
⊢ (riemannZeta (↑x : ℂ)).im = 0

Tactic:
(Complex.pos_iff.mp (riemannZeta_pos_of_one_lt hx)).2.symm

Premises used: riemannZeta_pos_of_one_lt, And.right, Complex.pos_iff, Iff.mp, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
h :
  ∀ (n : ℕ),
    ((fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) ⍟ fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) n = Complex.log (↑n : ℂ)
⊢ Eq (α := ℕ → ℂ) ((fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) ⍟ fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ))
    fun (n : ℕ) ↦ Complex.log (↑n : ℂ)

Tactic:
ext n
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
n : ℕ
⊢ ((fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) ⍟ fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) n = Complex.log (↑n : ℂ)

Tactic:
simpa [apply_ite, LSeries.convolution_def, -vonMangoldt_mul_zeta]
    using congr_arg (ofReal <| · n) vonMangoldt_mul_zeta

Premises used: LSeries.convolution_def, apply_ite, Complex.ofReal, congr_arg, ArithmeticFunction.vonMangoldt_mul_zeta
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
⊢ Eq (α := ℕ → ℂ) ((fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) ⍟ 1) fun (n : ℕ) ↦ Complex.log (↑n : ℂ)

Tactic:
(convolution_one_eq_convolution_zeta _).trans convolution_vonMangoldt_zeta

Premises used: LSeries.convolution_one_eq_convolution_zeta, ArithmeticFunction.convolution_vonMangoldt_zeta, Eq.trans
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
rw : 1 < (↑s.re : EReal)
⊢ abscissaOfAbsConv 1 < (↑s.re : EReal)

Tactic:
rw [abscissaOfAbsConv_one]

Premises used: LSeries.abscissaOfAbsConv_one
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ 1 < (↑s.re : EReal)

Tactic:
exact_mod_cast hs
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (logMul 1) s

Tactic:
have hf := LSeriesSummable_logMul_of_lt_re
    (show abscissaOfAbsConv 1 < s.re by rw [abscissaOfAbsConv_one]; exact_mod_cast hs)
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
hf : LSeriesSummable (logMul 1) s
rw :
  ∀ (hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term (logMul 1) s x‖),
    Summable (α := ℝ) fun (x : ℕ) ↦ ‖term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s x‖
⊢ LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s

Tactic:
rw [LSeriesSummable, ← summable_norm_iff] at hf ⊢

Premises used: summable_norm_iff, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term (logMul 1) s x‖
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ ‖term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s x‖

Tactic:
hf.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ norm_term_le s ?_)

Premises used: ArithmeticFunction.vonMangoldt, Summable.of_nonneg_of_le, Complex.ofReal, LSeries.term, LSeries.norm_term_le, DFunLike.coe, norm_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term (logMul 1) s x‖
refine : ∀ (n : ℕ), ‖(↑((Λ : (a : ℕ) → ℝ) n) : ℂ)‖ ≤ ‖logMul 1 n‖
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ ‖term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s x‖

Tactic:
refine hf.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ norm_term_le s ?_)

Premises used: Summable.of_nonneg_of_le, LSeries.norm_term_le, norm_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term (logMul 1) s x‖
n : ℕ
⊢ norm (E := ℂ) ((fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) n) ≤ ‖Complex.log (↑n : ℂ)‖

Tactic:
simpa [abs_of_nonneg, vonMangoldt_nonneg, ← natCast_log, Real.log_natCast_nonneg]
      using vonMangoldt_le_log

Premises used: Complex.natCast_log, Real.log_natCast_nonneg, ArithmeticFunction.vonMangoldt_nonneg, abs_of_nonneg, ArithmeticFunction.vonMangoldt_le_log
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term (logMul 1) s x‖
n : ℕ
⊢ norm (E := ℂ) ((fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) n) ≤ ‖Complex.log (↑n : ℂ)‖

Tactic:
have hΛ : ‖↗Λ n‖ ≤ ‖Complex.log n‖ := by
    simpa [abs_of_nonneg, vonMangoldt_nonneg, ← natCast_log, Real.log_natCast_nonneg]
      using vonMangoldt_le_log
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term (logMul 1) s x‖
n : ℕ
hΛ : norm (E := ℂ) ((fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) n) ≤ ‖Complex.log (↑n : ℂ)‖
⊢ ‖Complex.log (↑n : ℂ)‖ ≤ ‖logMul 1 n‖

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term (logMul 1) s x‖
n : ℕ
hΛ : norm (E := ℂ) ((fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) n) ≤ ‖Complex.log (↑n : ℂ)‖
⊢ ‖(↑((Λ : (a : ℕ) → ℝ) n) : ℂ)‖ ≤ ‖logMul 1 n‖

Tactic:
exact hΛ.trans <| by simp

Premises used: LE.le.trans
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
rw :
  ((HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
        (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) ⍟
      fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) =
    HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N))
      ((fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) ⍟ 1)
rw₁ :
  ((HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
        (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) ⍟
      fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) =
    (HMul.hMul (α := ℕ → ℂ) (fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) fun (n : ℕ) ↦
        (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) ⍟
      HMul.hMul (α := ℕ → ℂ) (fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) 1
rw₂ rw₃ :
  ((HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
        (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) ⍟
      fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) =
    (HMul.hMul (α := ℕ → ℂ) (fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) fun (n : ℕ) ↦
        (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) ⍟
      fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)
⊢ ((HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
        (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) ⍟
      fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) =
    HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦ Complex.log (↑n : ℂ)

Tactic:
rw [← convolution_vonMangoldt_const_one, ← χ.mul_convolution_distrib, mul_one]

Premises used: ArithmeticFunction.convolution_vonMangoldt_const_one, DirichletCharacter.mul_convolution_distrib, mul_one
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable
    (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
      (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
    s

Tactic:
LSeriesSummable_mul χ <| LSeriesSummable_vonMangoldt hs

Premises used: DirichletCharacter.LSeriesSummable_mul, ArithmeticFunction.LSeriesSummable_vonMangoldt
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
inl :
  ∀ (χ : DirichletCharacter ℂ 0),
    L
        (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0)) fun (n : ℕ) ↦
          (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
        s =
      -deriv (L fun (n : ℕ) ↦ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0)) s /
        L (fun (n : ℕ) ↦ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0)) s
inr :
  ∀ (hN : N ≠ 0),
    L
        (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
          (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
        s =
      -deriv (L fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s /
        L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
⊢ L
      (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
        (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
      s =
    -deriv (L fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s /
      L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s

Tactic:
rcases eq_or_ne N 0 with rfl | hN

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
hs : 1 < s.re
χ : DirichletCharacter ℂ 0
⊢ L
      (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0)) fun (n : ℕ) ↦
        (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
      s =
    -deriv (L fun (n : ℕ) ↦ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0)) s /
      L (fun (n : ℕ) ↦ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0)) s

Tactic:
simp [modZero_eq_delta, delta_mul_eq_smul_delta, LSeries_delta]

Premises used: LSeries_delta, LSeries.delta_mul_eq_smul_delta, DirichletCharacter.modZero_eq_delta
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
⊢ LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s

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