completedRiemannZeta_eq — Mathlib

English

The completed Riemann zeta function satisfies a standard decomposition: Λ(s) equals Λ₀(s) minus the simple pole corrections at s = 0 or s = 1, expressed as standard subtractions.

Русский

Завершённая функция Λ(s) раскладывается как Λ₀(s) минус простые полюсные поправки в s = 0 или s = 1.

LaTeX

$$$\\mathrm{completedRiemannZeta}(s) = \\mathrm{completedRiemannZeta}_0(s) - \\frac{1}{s} - \\frac{1}{1-s}$$$

Lean4

theorem completedRiemannZeta_eq (s : ℂ) : completedRiemannZeta s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s) := by
  simp_rw [completedRiemannZeta, completedRiemannZeta₀, completedHurwitzZetaEven_eq, if_true]

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