|
%I #17 Feb 07 2024 01:34:12
%S 5,4,6,3,0,6,8,3,5,9,5,2,4,8,2,7,4,1,7,3,6,0,9,8,7,6,9,6,2,4,1,0,1,3,
%T 8,8,9,3,7,6,3,5,5,3,9,0,8,1,6,5,9,1,3,5,4,1,6,7,8,3,3,9,9,1,7,6,1,6,
%U 3,6,8,9,8,4,1,1,9,6,5,7,6,7,6,1,7,4,1,2,2,1,6,3,4,1,0,3,9,5,4,6
%N Decimal expansion of Integral {x=0..infinity} 1/2^(2^x) dx.
%H I. S. Gradsteyn, I. M. Ryzhik, <a href="http://mathtable.com/gr/index.html">Table of integrals, series and products</a>, (1980) 8.212
%F -Ei(-log(2))/log(2), where Ei is the exponential integral function.
%F Also equals (2*Integral_{x = 0..1/2} log(log(1/x)) dx - log(log(2)))/(2*log(2)).
%F From _Peter Bala_, Feb 05 2024: (Start)
%F Equals 1/log(2) * Integral_{x >= 1} 1/(x * 2^x) dx.
%F Equals 1/log(4) * Integral_{x = 0..1} 1/(log(2) - log(x)) dx.
%F Equals Integral_{x >= 1} log(x)/2^x dx = (log(2))^2 * Integral_{x >= 0} x*(2^x) /(2^(2^x)). See Gradsteyn and Ryzhik, Section 8.212, formulas (4) and (16). (End)
%e 0.546306835952482741736098769624101388937635539081659135416783399176163689841...
%t RealDigits[-ExpIntegralEi[-Log[2]]/Log[2], 10, 100] // First
%o (PARI) eint1(log(2))/log(2) \\ _Charles R Greathouse IV_, Dec 02 2013
%Y Cf. A007400, A007404 (sum instead of integral).
%K nonn,cons
%O 0,1
%A _Jean-François Alcover_, Nov 29 2013
|
