awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
s : ℂ
hs : 1 < s.re
⊢ abscissaOfAbsConv 1 < (↑s.re : EReal)
have rw : 1 < (↑s.re : EReal)
Tactic: rw [abscissaOfAbsConv_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (hypothesis)
Goal:
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s
have hf : 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)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
s : ℂ
hs : 1 < s.re
hf : LSeriesSummable (logMul 1) s
⊢ LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s
have rw : ∀ (hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term (logMul 1) s x‖),
  Summable (α := ℝ) fun (x : ℕ) ↦ ‖term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s x‖
Tactic: rw [LSeriesSummable, ← summable_norm_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
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‖
have refine : ∀ (n : ℕ), ‖(↑((Λ : (a : ℕ) → ℝ) n) : ℂ)‖ ≤ ‖logMul 1 n‖
Tactic: refine hf.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ norm_term_le s ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (hypothesis)
Goal:
s : ℂ
hs : 1 < s.re
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term (logMul 1) s x‖
n : ℕ
⊢ ‖(↑((Λ : (a : ℕ) → ℝ) n) : ℂ)‖ ≤ ‖logMul 1 n‖
have hΛ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ 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 : ℂ)
have 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)
Tactic: rw [← convolution_vonMangoldt_const_one, ← χ.mul_convolution_distrib, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
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)
⊢ ((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 : ℂ)
have 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
Tactic: rw [← convolution_vonMangoldt_const_one, ← χ.mul_convolution_distrib, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
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
⊢ ((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 : ℂ)
have 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)
Tactic: rw [← convolution_vonMangoldt_const_one, ← χ.mul_convolution_distrib, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ 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
have 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
Tactic: rcases eq_or_ne N 0 with rfl | hN
Cleared hypotheses: N, χ
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
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
⊢ 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
have 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
Tactic: rcases eq_or_ne N 0 with rfl | hN
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
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
have hχ : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
Tactic: have hχ : LSeriesSummable ↗χ s := (LSeriesSummable_iff hN χ).mpr hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
⊢ (abscissaOfAbsConv fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) < (↑s.re : EReal)
have rwa : 1 < (↑s.re : EReal)
Tactic: rwa [absicssaOfAbsConv_eq_one hN, ← EReal.coe_one, EReal.coe_lt_coe_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
rwa : 1 < (↑s.re : EReal)
⊢ (abscissaOfAbsConv fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) < (↑s.re : EReal)
have rwa₁ : (↑1 : EReal) < (↑s.re : EReal)
Tactic: rwa [absicssaOfAbsConv_eq_one hN, ← EReal.coe_one, EReal.coe_lt_coe_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (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
have hs' : (abscissaOfAbsConv fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) < (↑s.re : EReal)
Tactic: have hs' : abscissaOfAbsConv ↗χ < s.re := by
    rwa [absicssaOfAbsConv_eq_one hN, ← EReal.coe_one, EReal.coe_lt_coe_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
hs' : (abscissaOfAbsConv fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) < (↑s.re : EReal)
⊢ 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
have hΛ : LSeriesSummable
  (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
    (↑((Λ : (a : ℕ) → ℝ) n) : ℂ))
  s
Tactic: have hΛ : LSeriesSummable (↗χ * ↗Λ) s := LSeriesSummable_twist_vonMangoldt χ hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
hs' : (abscissaOfAbsConv fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) < (↑s.re : EReal)
hΛ :
  LSeriesSummable
    (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
      (↑((Λ : (a : ℕ) → ℝ) 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
have inr : L (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦ Complex.log (↑n : ℂ)) s =
  L (logMul fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
s : ℂ
hs : 1 < s.re
⊢ L (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s = -deriv (L 1) s / L 1 s
have refine : ∀ {n : ℕ},
  n ≠ 0 →
    (↑((Λ : (a : ℕ) → ℝ) n) : ℂ) =
      HMul.hMul (α := ℕ → ℂ) (β := ℕ → ℂ) (fun (n : ℕ) ↦ (1 : (a : ZMod 1) → ℂ) (↑n : ZMod 1))
        (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) n
Tactic: refine (LSeries_congr (fun {n} _ ↦ ?_) s).trans <|
    LSeries_modOne_eq ▸ LSeries_twist_vonMangoldt_eq χ₁ hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
s : ℂ
hs : 1 < s.re
this : deriv (L 1) s = deriv riemannZeta s
⊢ L (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s = -deriv riemannZeta s / riemannZeta s
have rw : -deriv (L 1) s / L 1 s = -deriv riemannZeta s / riemannZeta s
Tactic: rw [LSeries_vonMangoldt_eq hs, ← LSeries_one_eq_riemannZeta hs, this]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
s : ℂ
hs : 1 < s.re
this : deriv (L 1) s = deriv riemannZeta s
rw : -deriv (L 1) s / L 1 s = -deriv riemannZeta s / riemannZeta s
⊢ L (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s = -deriv riemannZeta s / riemannZeta s
have rw₁ : -deriv (L 1) s / L 1 s = -deriv riemannZeta s / L 1 s
Tactic: rw [LSeries_vonMangoldt_eq hs, ← LSeries_one_eq_riemannZeta hs, this]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
s : ℂ
hs : 1 < s.re
this : deriv (L 1) s = deriv riemannZeta s
rw : -deriv (L 1) s / L 1 s = -deriv riemannZeta s / riemannZeta s
rw₁ : -deriv (L 1) s / L 1 s = -deriv riemannZeta s / L 1 s
⊢ L (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s = -deriv riemannZeta s / riemannZeta s
have rw₂ : -deriv riemannZeta s / L 1 s = -deriv riemannZeta s / L 1 s
Tactic: rw [LSeries_vonMangoldt_eq hs, ← LSeries_one_eq_riemannZeta hs, this]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
s : ℂ
hs : 1 < s.re
⊢ L (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) s = -deriv riemannZeta s / riemannZeta s
have suffices : deriv (L 1) s = deriv riemannZeta s
Tactic: suffices deriv (L 1) s = deriv riemannZeta s by
    rw [LSeries_vonMangoldt_eq hs, ← LSeries_one_eq_riemannZeta hs, this]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
s : ℂ
hs : 1 < s.re
⊢ deriv (L 1) s = deriv riemannZeta s
have refine : ∃ s_1 ∈ nhds s, Set.EqOn (L 1) riemannZeta s_1
Tactic: refine Filter.EventuallyEq.deriv_eq <| Filter.eventuallyEq_iff_exists_mem.mpr ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
χ : DirichletCharacter ℂ 1
⊢ LFunction χ = riemannZeta
have h : ∀ (x : ℂ), LFunction χ x = riemannZeta x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
χ : DirichletCharacter ℂ 1
x : ℂ
⊢ LFunction χ x = riemannZeta x
have h : ZMod.LFunction (N := 1) (⇑χ : (a : ZMod 1) → ℂ) x = riemannZeta x
Tactic: rw [LFunction, ZMod.LFunction_modOne_eq, (by rfl : (0 : ZMod 1) = 1), map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
χ : DirichletCharacter ℂ 1
x : ℂ
h : ZMod.LFunction (N := 1) (⇑χ : (a : ZMod 1) → ℂ) x = riemannZeta x
⊢ LFunction χ x = riemannZeta x
have h₁ : HMul.hMul (α := ℂ) ((χ : (a : ZMod 1) → ℂ) 0 : ℂ) (riemannZeta x) = riemannZeta x
Tactic: rw [LFunction, ZMod.LFunction_modOne_eq, (by rfl : (0 : ZMod 1) = 1), map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
χ : DirichletCharacter ℂ 1
x : ℂ
h : ZMod.LFunction (N := 1) (⇑χ : (a : ZMod 1) → ℂ) x = riemannZeta x
h₁ : HMul.hMul (α := ℂ) ((χ : (a : ZMod 1) → ℂ) 0 : ℂ) (riemannZeta x) = riemannZeta x
⊢ LFunction χ x = riemannZeta x
have h₂ : HMul.hMul (α := ℂ) ((χ : (a : ZMod 1) → ℂ) 1 : ℂ) (riemannZeta x) = riemannZeta x
Tactic: rw [LFunction, ZMod.LFunction_modOne_eq, (by rfl : (0 : ZMod 1) = 1), map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
χ : DirichletCharacter ℂ 1
x : ℂ
h : ZMod.LFunction (N := 1) (⇑χ : (a : ZMod 1) → ℂ) x = riemannZeta x
h₁ : HMul.hMul (α := ℂ) ((χ : (a : ZMod 1) → ℂ) 0 : ℂ) (riemannZeta x) = riemannZeta x
h₂ : HMul.hMul (α := ℂ) ((χ : (a : ZMod 1) → ℂ) 1 : ℂ) (riemannZeta x) = riemannZeta x
⊢ LFunction χ x = riemannZeta x
have h₃ : 1 * riemannZeta x = riemannZeta x
Tactic: rw [LFunction, ZMod.LFunction_modOne_eq, (by rfl : (0 : ZMod 1) = 1), map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
χ : DirichletCharacter ℂ 1
x : ℂ
h : ZMod.LFunction (N := 1) (⇑χ : (a : ZMod 1) → ℂ) x = riemannZeta x
h₁ : HMul.hMul (α := ℂ) ((χ : (a : ZMod 1) → ℂ) 0 : ℂ) (riemannZeta x) = riemannZeta x
h₂ : HMul.hMul (α := ℂ) ((χ : (a : ZMod 1) → ℂ) 1 : ℂ) (riemannZeta x) = riemannZeta x
h₃ : 1 * riemannZeta x = riemannZeta x
⊢ LFunction χ x = riemannZeta x
have h₄ : riemannZeta x = riemannZeta x
Tactic: rw [LFunction, ZMod.LFunction_modOne_eq, (by rfl : (0 : ZMod 1) = 1), map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ deriv (LFunction χ) s = deriv (LSeries fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) s
have refine : LFunction χ =ᶠ[𝓝 s] LSeries fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)
Tactic: refine Filter.EventuallyEq.deriv_eq ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (hypothesis)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ LFunction χ =ᶠ[𝓝 s] LSeries fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)
have h : {z : ℂ | 1 < z.re} ∈ 𝓝 s
Tactic: have h : {z | 1 < z.re} ∈ nhds s :=
    (isOpen_lt continuous_const continuous_re).mem_nhds hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : {z : ℂ | 1 < z.re} ∈ 𝓝 s
⊢ LFunction χ =ᶠ[𝓝 s] LSeries fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)
have h₁ : ∀ (z : ℂ) (hz : 1 < z.re), LFunction χ z = LSeries (fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) z
Tactic: filter_upwards [h] with z hz
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.Even
n : ℕ
inst_1 : NeZero n
⊢ LFunction χ (-HMul.hMul (α := ℂ) 2 (↑n : ℂ)) = 0
have obtain : ∀ (m : ℕ) [NeZero m.succ], LFunction χ (-HMul.hMul (α := ℂ) 2 (↑m.succ : ℂ)) = 0
Tactic: obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)
Cleared hypotheses: n, inst_1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (hypothesis)
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
⊢ LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ) s =
    LFunction χ s *
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
have hpc : IsPreconnected (α := ℂ) {1}ᶜ
Tactic: have hpc : IsPreconnected ({1}ᶜ : Set ℂ) :=
    (isConnected_compl_singleton_of_one_lt_rank (rank_real_complex ▸ Nat.one_lt_ofNat) _)
      |>.isPreconnected
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (hypothesis)
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
⊢ LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ) s =
    LFunction χ s *
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
have hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
Tactic: have hne : 2 ∈ ({1}ᶜ : Set ℂ) := by simp
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
⊢ LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ) s =
    LFunction χ s *
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
have refine_1 : AnalyticOnNhd ℂ (LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ)) {1}ᶜ
Tactic: refine AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq (𝕜 := ℂ)
    (g := fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))) ?_ ?_ hpc hne ?_ hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
refine_1 :
  AnalyticOnNhd ℂ (LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ))
    {1}ᶜ
⊢ LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ) s =
    LFunction χ s *
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
have refine_2 : AnalyticOnNhd ℂ (F := ℂ)
  (fun (s : ℂ) ↦
    LFunction χ s *
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
  {1}ᶜ
Tactic: refine AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq (𝕜 := ℂ)
    (g := fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))) ?_ ?_ hpc hne ?_ hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
refine_1 :
  AnalyticOnNhd ℂ (LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ))
    {1}ᶜ
refine_2 :
  AnalyticOnNhd ℂ (F := ℂ)
    (fun (s : ℂ) ↦
      LFunction χ s *
        ∏ p ∈ N.primeFactors,
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
    {1}ᶜ
⊢ LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ) s =
    LFunction χ s *
      ∏ p ∈ N.primeFactors,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
have refine_3 : LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ) =ᶠ[𝓝 2] fun (s : ℂ) ↦
  LFunction χ s *
    ∏ p ∈ N.primeFactors,
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
Tactic: refine AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq (𝕜 := ℂ)
    (g := fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))) ?_ ?_ hpc hne ?_ hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
⊢ AnalyticOnNhd ℂ (LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ))
    {1}ᶜ
have refine_1 : ∀ (s : ℂ) (hs : Membership.mem (γ := Set ℂ) {1}ᶜ s),
  DifferentiableWithinAt ℂ
    (LFunction (N := N) ((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ)) {1}ᶜ s
Tactic: refine DifferentiableOn.analyticOnNhd (fun s hs ↦ ?_) isOpen_compl_singleton
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
M N : ℕ
inst : NeZero M
inst_1 : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected (α := ℂ) {1}ᶜ
hne : Membership.mem (γ := Set ℂ) {1}ᶜ 2
⊢ AnalyticOnNhd ℂ (F := ℂ)
    (fun (s : ℂ) ↦
      LFunction χ s *
        ∏ p ∈ N.primeFactors,
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
    {1}ᶜ
have refine_2 : ∀ (s : ℂ) (hs : Membership.mem (γ := Set ℂ) {1}ᶜ s),
  DifferentiableWithinAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦
      LFunction χ s *
        ∏ p ∈ N.primeFactors,
          (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
    {1}ᶜ s
Tactic: refine DifferentiableOn.analyticOnNhd (fun s hs ↦ ?_) isOpen_compl_singleton