awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
⊢ (hurwitzEvenFEPair (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)).symm.Λ (s / 2) / 2 =
    HDiv.hDiv (α := ℂ) (mellin (fun (t : ℝ) ↦ (↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) (s / 2)) 2
have e_a : (hurwitzEvenFEPair (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)).symm.Λ (s / 2) =
  mellin (fun (t : ℝ) ↦ (↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) (s / 2)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
⊢ (hurwitzEvenFEPair (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)).symm.Λ (s / 2) =
    mellin (fun (t : ℝ) ↦ (↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) (s / 2)
have e_a : 1 / 2 < (s / 2).re
Tactic: refine ((hurwitzEvenFEPair a).symm.hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
⊢ 1 / 2 < (s / 2).re
have e_a : 1 / 2 < s.re / 2
Tactic: rwa [div_ofNat_re, div_lt_div_iff_of_pos_right two_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
⊢ HasSum (fun (n : ℤ) ↦ s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have rw : HasSum (α := ℂ)
  (fun (n : ℤ) ↦ s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
  (mellin (fun (t : ℝ) ↦ ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2) (s / 2))
Tactic: rw [show completedCosZeta a s = mellin (fun t ↦ (cosKernel a t - 1 : ℂ) / 2) (s / 2) by
    rw [mellin_div_const, completedCosZeta]
    congr 1
    refine ((hurwitzEvenFEPair a).symm.hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm
    rwa [div_ofNat_re, div_lt_div_iff_of_pos_right two_pos]]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
⊢ HasSum (α := ℂ)
    (fun (n : ℤ) ↦ s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (mellin (fun (t : ℝ) ↦ ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2) (s / 2))
have refine_1 : Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
Tactic: refine (hasSum_mellin_pi_mul_sq (zero_lt_one.trans hs) hF ?_).congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
refine_1 : Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
⊢ HasSum (α := ℂ)
    (fun (n : ℤ) ↦ s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (mellin (fun (t : ℝ) ↦ ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2) (s / 2))
have refine_2 : ∀ (n : ℤ),
  s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
    s.Gammaℝ * c n / (↑|(↑n : ℝ)| : ℂ) ^ s
Tactic: refine (hasSum_mellin_pi_mul_sq (zero_lt_one.trans hs) hF ?_).congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
have refine_1 : ∀ (i : ℤ), ‖‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re‖ ≤ 1 / |HAdd.hAdd (α := ℝ) (↑i : ℝ) 0| ^ s.re / 2
Tactic: apply (((summable_one_div_int_add_rpow 0 s.re).mpr hs).div_const 2).of_norm_bounded
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
i : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑i : ℂ) = (↑(2 * π * a * (↑i : ℝ)) : ℂ) * I
have push_cast : 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑i : ℂ) = 2 * (↑π : ℂ) * (↑a : ℂ) * (↑i : ℂ) * I
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
i : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑i : ℂ) = (↑(2 * π * a * (↑i : ℝ)) : ℂ) * I
have ring : 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑i : ℂ) = 2 * (↑π : ℂ) * (↑a : ℂ) * (↑i : ℂ) * I
Tactic: { push_cast; ring }
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
have rw : HPow.hPow (α := ℂ) (↑0 : ℂ) s = 0
Tactic: rw [abs_zero, Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
rw : HPow.hPow (α := ℂ) (↑0 : ℂ) s = 0
⊢ HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
have rw₁ : HPow.hPow (α := ℂ) 0 s = 0
Tactic: rw [abs_zero, Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
rw : HPow.hPow (α := ℂ) (↑0 : ℂ) s = 0
rw₁ : HPow.hPow (α := ℂ) 0 s = 0
⊢ HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
have rw₂ : Eq (α := ℂ) 0 0
Tactic: rw [abs_zero, Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum
    (fun (n : ℕ) ↦
      if n = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
Tactic: have aux : ((|0| : ℤ) : ℂ) ^ s = 0 := by
    rw [abs_zero, Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
⊢ HasSum
    (fun (n : ℕ) ↦
      if n = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have hint : HasSum
  (fun (n : ℕ) ↦
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
        2)
  (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s +
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) / HPow.hPow (α := ℂ) (↑|0| : ℂ) s / 2)
Tactic: have hint := (hasSum_int_completedCosZeta a hs).nat_add_neg
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
hint :
  HasSum
    (fun (n : ℕ) ↦
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s +
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) / HPow.hPow (α := ℂ) (↑|0| : ℂ) s / 2)
⊢ HasSum
    (fun (n : ℕ) ↦
      if n = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have hint₁ : HasSum
  (fun (n : ℕ) ↦
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
        2)
  (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
Tactic: rw [aux, div_zero, zero_div, add_zero] at hint
Cleared hypotheses: hint
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
hint :
  HasSum
    (fun (n : ℕ) ↦
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
⊢ HasSum
    (fun (n : ℕ) ↦
      if n = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have refine : ∀ (n : ℕ),
  (if n = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s) =
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s / 2
Tactic: refine hint.congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
hint :
  HasSum
    (fun (n : ℕ) ↦
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
⊢ (if n = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s) =
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s / 2
have pos : ∀ (h : n = 0),
  0 =
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s / 2
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
hint :
  HasSum
    (fun (n : ℕ) ↦
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
pos :
  ∀ (h : n = 0),
    0 =
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2
⊢ (if n = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s) =
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s / 2
have neg : ∀ (h : ¬n = 0),
  s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s / 2
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
⊢ HasSum
    (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ))
    (((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
        (↑(if
                Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                  (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
              1
            else 0) :
          ℂ)) /
      2)
have refine : ∀ (n : ℤ),
  (if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ)) =
    (↑(if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
Tactic: refine (ofReal_sub .. ▸ (hasSum_ofReal.mpr (hasSum_int_evenKernel₀ a ht)).div_const
      2).congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
⊢ (if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ)) =
    (↑(if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
have pos : (↑n : ℝ) + a = 0 → 0 = (↑0 : ℂ) / 2
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
pos : (↑n : ℝ) + a = 0 → 0 = (↑0 : ℂ) / 2
⊢ (if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ)) =
    (↑(if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
have neg : ¬(↑n : ℝ) + a = 0 →
  1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) =
    (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
h : (↑n : ℝ) + a = 0
⊢ 0 = (↑0 : ℂ) / 2
have pos : 0 = 0 / 2
Tactic: rw [ofReal_zero, zero_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
h : (↑n : ℝ) + a = 0
pos : 0 = 0 / 2
⊢ 0 = (↑0 : ℂ) / 2
have pos₁ : Eq (α := ℂ) 0 0
Tactic: rw [ofReal_zero, zero_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
h : ¬(↑n : ℝ) + a = 0
⊢ 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) =
    (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
have neg : (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) * (1 / 2) =
  (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
Tactic: rw [mul_comm, mul_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
h : ¬(↑n : ℝ) + a = 0
neg :
  (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) * (1 / 2) =
    (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
⊢ 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) =
    (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
have neg₁ : (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2 =
  (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
Tactic: rw [mul_comm, mul_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun (n : ℤ) ↦ s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have hF : ∀ (t : ℝ) (ht : 0 < t),
  HasSum
    (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ))
    (((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
        (↑(if
                Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                  (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
              1
            else 0) :
          ℂ)) /
      2)
Tactic: have hF (t : ℝ) (ht : 0 < t) : HasSum (fun n : ℤ ↦ if n + a = 0 then 0
      else (1 / 2 : ℂ) * rexp (-π * (n + a) ^ 2 * t))
      ((evenKernel a t - (if (a : UnitAddCircle) = 0 then 1 else 0 : ℝ)) / 2) := by
    refine (ofReal_sub .. ▸ (hasSum_ofReal.mpr (hasSum_int_evenKernel₀ a ht)).div_const
      2).congr_fun fun n ↦ ?_
    split_ifs
    · rw [ofReal_zero, zero_div]
    · rw [mul_comm, mul_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ))
      (((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
          (↑(if
                  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                    (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                1
              else 0) :
            ℂ)) /
        2)
⊢ completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s =
    mellin
      (fun (t : ℝ) ↦
        ((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
            (↑(if
                    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                      (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                  1
                else 0) :
              ℂ)) /
          2)
      (s / 2)
have simp_rw : completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s =
  HDiv.hDiv (α := ℂ)
    (mellin
      (fun (t : ℝ) ↦
        (↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
          if
              Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
            1
          else 0)
      (s / 2))
    2
Tactic: simp_rw [mellin_div_const, apply_ite ofReal, ofReal_one, ofReal_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ))
      (((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
          (↑(if
                  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                    (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                1
              else 0) :
            ℂ)) /
        2)
⊢ completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s =
    HDiv.hDiv (α := ℂ)
      (mellin
        (fun (t : ℝ) ↦
          (↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
            if
                Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                  (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
              1
            else 0)
        (s / 2))
      2
have refine : 1 / 2 < (s / 2).re
Tactic: refine congr_arg (· / 2) ((hurwitzEvenFEPair a).hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ))
      (((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
          (↑(if
                  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                    (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                1
              else 0) :
            ℂ)) /
        2)
⊢ 1 / 2 < (s / 2).re
have rwa : 1 / 2 < s.re / 2
Tactic: rwa [div_ofNat_re, div_lt_div_iff_of_pos_right two_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ))
      (((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
          (↑(if
                  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                    (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                1
              else 0) :
            ℂ)) /
        2)
⊢ HasSum (fun (n : ℤ) ↦ s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have rw : HasSum (α := ℂ) (fun (n : ℤ) ↦ s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
  (mellin
    (fun (t : ℝ) ↦
      ((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
          (↑(if
                  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                    (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                1
              else 0) :
            ℂ)) /
        2)
    (s / 2))
Tactic: rw [show completedHurwitzZetaEven a s = mellin (fun t ↦ ((evenKernel (↑a) t : ℂ) -
        ↑(if (a : UnitAddCircle) = 0 then 1 else 0 : ℝ)) / 2) (s / 2) by
    simp_rw [mellin_div_const, apply_ite ofReal, ofReal_one, ofReal_zero]
    refine congr_arg (· / 2) ((hurwitzEvenFEPair a).hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm
    rwa [div_ofNat_re, div_lt_div_iff_of_pos_right two_pos]]