completedRiemannZeta_one — Mathlib

English

The completed zeta function Λ satisfies Λ(1) = (γ − log(4π))/2.

Русский

Улучшенная дзета-функция Λ удовлетворяет Λ(1) = (γ − log(4π))/2.

LaTeX

$$$$ \Lambda(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_.completedRiemannZeta_one : completedRiemannZeta 1 = (γ - Complex.log (4 * ↑π)) / 2 :=
  (riemannZeta_one ▸ div_one (_ : ℂ) ▸ Gammaℝ_one ▸ riemannZeta_def_of_ne_zero one_ne_zero).symm

Похожие утверждения