English
For hk ≠ 0 and x ∈ [0,1], hurwitzZetaOdd(x, −(2k+1)) = 0; i.e., odd negative integers are zeros of hurwitzZetaOdd.
Русский
Для hk ≠ 0 и x ∈ [0,1], hurwitzZetaOdd(x, −(2k+1)) = 0; нечетные отрицательные аргументы являются нулями hurwitzZetaOdd.
LaTeX
$$$$ \mathrm{hurwitzZetaOdd}(x, -(2k+1)) = 0, \quad \forall k\in\mathbb{N}, \; x\in[0,1]. $$$$
Lean4
theorem hurwitzZetaOdd_neg_two_mul_nat (hk : k ≠ 0) (hx : x ∈ Icc (0 : ℝ) 1) :
hurwitzZetaOdd x (-(2 * k)) =
-1 / (2 * k + 1) * ((Polynomial.bernoulli (2 * k + 1)).map (algebraMap ℚ ℂ)).eval (x : ℂ) :=
by
have h1 (n : ℕ) : (2 * k + 1 : ℂ) ≠ -n :=
by
rw [← Int.cast_ofNat, ← Int.cast_natCast, ← Int.cast_mul, ← Int.cast_natCast n, ← Int.cast_neg, ← Int.cast_one, ←
Int.cast_add, Ne, Int.cast_inj, ← Ne]
refine ne_of_gt ((neg_nonpos_of_nonneg n.cast_nonneg).trans_lt ?_)
positivity
have h3 : Gammaℂ (2 * k + 1) ≠ 0 :=
by
refine mul_ne_zero (mul_ne_zero two_ne_zero ?_) (Gamma_ne_zero h1)
simp [pi_ne_zero]
rw [(by simp : -(2 * k : ℂ) = 1 - (2 * k + 1)), hurwitzZetaOdd_one_sub _ h1, ← Gammaℂ,
sinZeta_two_mul_nat_add_one' hk hx, ← mul_assoc, ← mul_div_assoc, mul_assoc, mul_div_cancel_left₀ _ h3, ←
mul_div_assoc]
congr 2
rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast, ← ofReal_one, ← ofReal_ofNat, ←
ofReal_div, ← ofReal_add, ← ofReal_mul, ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div,
Real.sin_add_pi_div_two, ← sub_zero (k * π), cos_nat_mul_pi_sub, Real.cos_zero, mul_one, ofReal_pow, ofReal_neg,
ofReal_one, pow_succ, mul_neg_one, mul_neg, ← mul_pow, neg_one_mul, neg_neg, one_pow]
-- private because it is superseded by `hurwitzZeta_neg_nat` below
