English
The completed odd Hurwitz zeta is odd in its first argument: completedHurwitzZetaOdd(-a, s) = - completedHurwitzZetaOdd(a, s).
Русский
Завершенная нечетная Хёрвитц ζ-функция нечетна по первому аргументу: completedHurwitzZetaOdd(-a, s) = - completedHurwitzZetaOdd(a, s).
LaTeX
$$$$ completedHurwitzZetaOdd(-a, s) = - completedHurwitzZetaOdd(a, s). $$$$
Lean4
/-- Formula for `completedHurwitzZetaOdd` as a Dirichlet series in the convergence range. -/
theorem hasSum_int_completedHurwitzZetaOdd (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℤ ↦ Gammaℝ (s + 1) * SignType.sign (n + a) / (↑|n + a| : ℂ) ^ s / 2)
(completedHurwitzZetaOdd a s) :=
by
let r (n : ℤ) : ℝ := n + a
let c (n : ℤ) : ℂ := 1 / 2
have hF t (ht : 0 < t) : HasSum (fun n ↦ c n * r n * rexp (-π * (r n) ^ 2 * t)) (oddKernel a t / 2) :=
by
refine ((hasSum_ofReal.mpr (hasSum_int_oddKernel a ht)).div_const 2).congr_fun fun n ↦ ?_
simp [r, c, push_cast, div_mul_eq_mul_div, -one_div]
have h_sum : Summable fun i ↦ ‖c i‖ / |r i| ^ s.re :=
by
simp_rw [c, ← mul_one_div ‖_‖]
apply Summable.mul_left
rwa [summable_one_div_int_add_rpow]
have := mellin_div_const .. ▸ hasSum_mellin_pi_mul_sq' (zero_lt_one.trans hs) hF h_sum
refine this.congr_fun fun n ↦ ?_
simp only [r, c, mul_one_div, div_mul_eq_mul_div, div_right_comm]
