English
The variant Λ0 satisfies Λ0(1) = (γ − log(4π))/2 + 1.
Русский
Вариант Λ0 удовлетворяет Λ0(1) = (γ − log(4π))/2 + 1.
LaTeX
$$$$ \Lambda_0(1) = \frac{\gamma - \log(4\pi)}{2} + 1. $$$$
Lean4
/-- Formula for `Λ₀ 1`, where `Λ₀` is the entire function satisfying
`Λ₀ s = π ^ (-s / 2) Γ(s / 2) ζ(s) + 1 / s + 1 / (1 - s)` away from `s = 0, 1`.
Note that `s = 1` is _not_ a pole of `Λ₀`, so this statement (unlike `riemannZeta_one`) is
a mathematically meaningful statement and is not dependent on Mathlib's particular conventions for
division by zero. -/
theorem _root_.completedRiemannZeta₀_one : completedRiemannZeta₀ 1 = (γ - Complex.log (4 * ↑π)) / 2 + 1 :=
by
have := completedRiemannZeta_eq 1
rw [sub_self, div_zero, div_one, sub_zero, eq_sub_iff_add_eq] at this
rw [← this, completedRiemannZeta_one]
