English
The value of the Riemann zeta function at 1 is the finite expression (γ − log(4π))/2, understood in the constructed sense.
Русский
Значение дзета-функции Римана в точке 1 равно (γ − log(4π))/2 в принятых нами конвенциях.
LaTeX
$$$$ \zeta(1) = \frac{\gamma - \log(4\pi)}{2}. $$$$
Lean4
/-- Formula for `ζ 1`. Note that mathematically `ζ 1` is undefined, but our construction ascribes
this particular value to it. -/
theorem _root_.riemannZeta_one : riemannZeta 1 = (γ - Complex.log (4 * ↑π)) / 2 :=
by
have := (HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_one 0).mono_left <| nhdsWithin_le_nhds (s := { 1 }ᶜ)
simp only [HurwitzZeta.hurwitzZetaEven_zero, div_right_comm _ _ (Gammaℝ _)] at this
exact tendsto_nhds_unique this tendsto_riemannZeta_sub_one_div_Gammaℝ
