cp's OEIS Frontend

A380908 Decimal expansion of lim_{s->1} (zeta(s) - Pi^(s/2)/((s-1)*Gamma(s/2))) (negated).

%I A380908 #20 Sep 03 2025 00:04:45
%S A380908 9,7,6,9,0,4,2,9,1,0,3,3,8,7,8,9,6,6,1,8,5,6,8,9,7,5,2,0,9,3,5,0,4,7,
%T A380908 0,8,3,7,8,0,6,7,8,7,2,8,4,7,9,4,9,2,4,0,4,7,4,6,0,7,9,2,7,7,8,7,0,2,
%U A380908 8,6,4,3,5,2,3,2,7,5,4,2,0,0,2,9,2,0,1,4,3,0,4,8,8,2,9
%N A380908 Decimal expansion of lim_{s->1} (zeta(s) - Pi^(s/2)/((s-1)*Gamma(s/2))) (negated).
%C A380908 This limit is Mathlib's definition of the 'completed Riemann zeta function' at s = 1. Mathematically zeta(1) is undefined; for the 'completed zeta function' the above limit value is assigned by construction (see Loeffler&Stoll). Such a value is also called a 'junk value' in several proof systems.
%H A380908 Paolo Xausa, <a href="/A380908/b380908.txt">Table of n, a(n) for n = 0..10000</a>
%H A380908 David Loeffler and Michael Stoll, <a href="https://doi.org/10.48550/arXiv.2503.00959">Formalizing zeta and L-functions in Lean</a>, arXiv:2503.00959 [math.NT], March 2025.
%H A380908 Mathlib4, <a href="https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/Harmonic/ZetaAsymp.html#completedRiemannZeta_one">Value of the completed Riemann zeta at s = 1</a>.
%H A380908 Wikipedia, <a href="https://en.wikipedia.org/wiki/Lean_(proof_assistant)">Lean (proof assistant)</a>, March 2025.
%F A380908 Equals (gamma - log(4*Pi))/2.
%F A380908 Equals gamma + Psi(1/2)/2 - log(Pi^(1/2)) = A001620 - A114864 - A155968.
%e A380908 -0.976904291033878966185689752093504708378...
%p A380908 c := -(gamma - log(4*Pi))/2: evalf(c, 110)*10^95: ListTools:-Reverse(convert(floor(%), base, 10));
%t A380908 First[RealDigits[(EulerGamma - Log[4*Pi])/2, 10, 100]] (* _Paolo Xausa_, Mar 05 2025 *)
%o A380908 (PARI) (Euler-log(4*Pi))/2 \\ _Charles R Greathouse IV_, Sep 03 2025
%Y A380908 Cf. A001620, A114864, A155968.
%K A380908 nonn,cons,changed
%O A380908 0,1
%A A380908 _Peter Luschny_, Mar 04 2025