A Computer-Aided Proof of a Corrected Version of 10.2.32 in Abramowitz & Stegun's HMSNiMvLUklZXZhbEdJKnByb3RlY3RlZEdGJjYkLUklZGlmZkdGJjYkLSZJIklHNiI2I0kjbnVHRi42I0kieEdGLkYwL0YwKiYiIiJGNSIiIyEiIiwkKiYsJiomLSZJIkVHRi42I0Y1NiMqJkY2RjVGMkY1RjUtSSRleHBHNiRGJkkoX3N5c2xpYkdGLkYxRjVGNSomLUkjRWlHRkRGQEY1LUZDNiMsJEYyRjdGNUY1RjUtSSVzcXJ0R0ZENiMqKEY2RjVJI1BpR0YmRjVGMkY1RjdGNw==Fr\351d\351ric Chyzak (June 10, 2005)This session has been prepared with Maple9.5 and no additional library.For simplicity of treatment, we restrict ourselves to positive real NiNJInhHNiI=. Discussing the identity on other domains requires handling branch cuts; see the concluding remarks. Note that for NiMyIiIhSSJ4RzYi and in traditional notation (A&S), NiMvLSZJIkVHNiI2IyIiIjYjSSJ4R0YnLCQtSSNFaUc2JEkqcHJvdGVjdGVkR0YwSShfc3lzbGliR0YnNiMsJEYrISIiRjQ=. This also equals the value NiMtSSNFaUc2JEkqcHJvdGVjdGVkR0YmSShfc3lzbGliRzYiNiQiIiJJInhHRig= in Maple notation. The right-hand side of the identity under study therefore is:fo:=-1/sqrt(2)/sqrt(Pi)/sqrt(x)*(Ei(2*x)*exp(-x)-Ei(-2*x)*exp(x));

NiM+SSNmb0c2IiwkKioiIiMjIiIiRihJI1BpR0kqcHJvdGVjdGVkR0YsIyEiIkYoSSJ4R0YlRi0sJiomLUkjRWlHNiRGLEkoX3N5c2xpYkdGJTYjLCRGL0YoRiotSSRleHBHRjQ2IywkRi9GLkYqRioqJi1GMzYjLCRGLyEiI0YqLUY5NiNGL0YqRi5GKkYt

Start with the ODE satisfied by NiMtJkkiSUc2IjYjSSNudUdGJjYjSSJ4R0Ym.deq1:=x^2*diff(y(x),x,x)+x*diff(y(x),x)-(x^2+nu^2)*y(x);

NiM+SSVkZXExRzYiLCgqJkkieEdGJSIiIy1JJWRpZmZHSSpwcm90ZWN0ZWRHRiw2JC1JInlHRiU2I0YoLUkiJEdGLDYkRihGKSIiIkY0KiZGKEY0LUYrNiRGLkYoRjRGNComLCYqJEYoRilGNCokSSNudUdGJUYpRjRGNEYuRjQhIiI=

dsolve(deq1,y(x));

NiMvLUkieUc2IjYjSSJ4R0YmLCYqJkkkX0MxR0YmIiIiLUkoQmVzc2VsSUc2JEkqcHJvdGVjdGVkR0YwSShfc3lzbGliR0YmNiRJI251R0YmRihGLEYsKiZJJF9DMkdGJkYsLUkoQmVzc2VsS0dGL0YyRixGLA==

Taking derivative with respect to NiNJI251RzYi allows us to get an inhomogeneous ODE in NiMtSSVkaWZmR0kqcHJvdGVjdGVkR0YlNiQtJkkiSUc2IjYjSSNudUdGKjYjSSJ4R0YqRiw= with right-hand side in terms of NiMtJkkiSUc2IjYjSSNudUdGJjYjSSJ4R0Ym.deq2:=diff(deq1,nu)+eval(deq1,y(x)=z(x));

NiM+SSVkZXEyRzYiLCoqJkkjbnVHRiUiIiItSSJ5R0YlNiNJInhHRiVGKSEiIyomRi0iIiMtSSVkaWZmR0kqcHJvdGVjdGVkR0YzNiQtSSJ6R0YlRiwtSSIkR0YzNiRGLUYwRilGKSomRi1GKS1GMjYkRjVGLUYpRikqJiwmKiRGLUYwRikqJEYoRjBGKUYpRjVGKSEiIg==

The next step is a (differential) elimination of NiMtSSJ5RzYiNiNJInhHRiU= (and possibly of its derivatives) between NiNJJWRlcTFHNiI= and NiNJJWRlcTJHNiI=. To this end, an annihilating operator for the term in NiNJJWRlcTJHNiI= that involves NiMtSSJ5RzYiNiNJInhHRiU= can in the general situation be obtained by existing code (Mgfun[dfinite_expr_to_diffeq]). Here, this term is so simple that no computation is required. Upon applying its annihilating operator, we get a homogeneous ODE in NiMtSSVkaWZmR0kqcHJvdGVjdGVkR0YlNiQtJkkiSUc2IjYjSSNudUdGKjYjSSJ4R0YqRiw=.collect(eval(deq1,y(x)=deq2)+2*nu*deq1,{z,diff},factor);

NiMsLCooSSJ4RzYiIiIiLCgqJEYlIiIjIiInISIiRicqJEkjbnVHRiZGKkYqRictSSVkaWZmR0kqcHJvdGVjdGVkR0YxNiQtSSJ6R0YmNiNGJUYlRidGLCooRiVGKiwoISIoRidGKUYqRi1GKkYnLUYwNiRGMy1JIiRHRjE2JEYlRipGJ0YsKiZGJSIiJC1GMDYkRjMtRjw2JEYlRj9GJ0YrKiZGJSIiJS1GMDYkRjMtRjw2JEYlRkVGJ0YnKigsKEYtRidGJUYqRilGJ0YnLChGLUYnRiUhIiNGKUYnRidGM0YnRic=

The relation to be obtained is for NiMvSSNudUc2IiomIiIiRiciIiMhIiI=, and the ODE becomes:deq:=collect(16*eval(%,nu=1/2),{z,diff},factor);

NiM+SSRkZXFHNiIsLCooSSJ4R0YlIiIiLCYqJEYoIiIjIiM3ISIiRilGKS1JJWRpZmZHSSpwcm90ZWN0ZWRHRjE2JC1JInpHRiU2I0YoRihGKSEiKSooRihGLCwmISM4RilGKyIiJUYpLUYwNiRGMy1JIiRHRjE2JEYoRixGKUY2KiZGKCIiJC1GMDYkRjMtRj42JEYoRkFGKSIjJyoqJkYoRjotRjA2JEYzLUY+NiRGKEY6RikiIzsqKCwoRilGKUYoIiIpRitGOkYpLChGKUYpRihGNkYrRjpGKUYzRilGKQ==

We easily check that NiMtSSVldmFsR0kqcHJvdGVjdGVkR0YlNiQtSSVkaWZmR0YlNiQtJkkiSUc2IjYjSSNudUdGLTYjSSJ4R0YtRi8vRi8qJiIiIkY0IiIjISIi is a solution to this equation: by inserting NiMtJkkiSUc2IjYjSSNudUdGJjYjSSJ4R0Ym into it, we get a double zero at NiMvSSNudUc2IiomIiIiRiciIiMhIiI=.factor(simplify(eval(deq,z(x)=BesselI(nu,x))));

NiMqKC1JKEJlc3NlbElHNiRJKnByb3RlY3RlZEdGJ0koX3N5c2xpYkc2IjYkSSNudUdGKUkieEdGKSIiIiwmRisiIiMhIiJGLUYvLCZGK0YvRi1GLUYv

At this point, we readily verify that the right-hand side of BS.37.6 is also a solution of the differential equation NiNJJGRlcUc2Ig==.simplify(eval(deq,z(x)=fo));

NiMiIiE=

Better than just verifying the identity, we want to derive it by computing the right-hand side from the left-hand side. This is done by comparing initial conditions. The general solution of the ODE isdsolve(deq);

NiMvLUkiekc2IjYjSSJ4R0YmLCoqKEkkX0MxR0YmIiIiRigjISIiIiIjLUkkZXhwRzYkSSpwcm90ZWN0ZWRHRjNJKF9zeXNsaWJHRiZGJ0YsRiwqKEkkX0MyR0YmRixGKEYtLUYxNiMsJEYoRi5GLEYsKipJJF9DM0dGJkYsRihGLUYwRiwtSSNFaUdGMjYkRiwsJEYoRi9GLEYsKipJJF9DNEdGJkYsRihGLUY3RiwtRj02JEYsLCRGKCEiI0YsRiw=

Here, for positive NiNJInhHNiI=, we have both relations NiMvLUkjRWlHNiRJKnByb3RlY3RlZEdGJ0koX3N5c2xpYkc2IjYkIiIiSSJ4R0YpLCQtRiU2IywkRiwhIiJGMQ== and NiMvLUkjRWlHNiRJKnByb3RlY3RlZEdGJ0koX3N5c2xpYkc2IjYkIiIiLCRJInhHRikhIiIsJi1GJTYjRi1GLiomSSJJR0YpRitJI1BpR0YnRitGLg==, so that, up to a change of the constants in the general solution above, we may replace it withdsol:=_C1*exp(x)/sqrt(x)+_C2*exp(-x)/sqrt(x)+_C3*Ei(-2*x)*exp(x)/sqrt(x)+_C4*Ei(2*x)*exp(-x)/sqrt(x);

NiM+SSVkc29sRzYiLCoqKEkkX0MxR0YlIiIiSSJ4R0YlIyEiIiIiIy1JJGV4cEc2JEkqcHJvdGVjdGVkR0YxSShfc3lzbGliR0YlNiNGKkYpRikqKEkkX0MyR0YlRilGKkYrLUYvNiMsJEYqRixGKUYpKipJJF9DM0dGJUYpLUkjRWlHRjA2IywkRiohIiNGKUYuRilGKkYrRikqKkkkX0M0R0YlRiktRjw2IywkRipGLUYpRjZGKUYqRitGKQ==

Summarizing, we have obtained the following fourth-order ODE satisfied by NiMtSSVldmFsR0kqcHJvdGVjdGVkR0YlNiQtSSVkaWZmR0YlNiQtJkkiSUc2IjYjSSNudUdGLTYjSSJ4R0YtRi8vRi8qJiIiIkY0IiIjISIi as well as its general solution:

deq;

NiMsLCooSSJ4RzYiIiIiLCYqJEYlIiIjIiM3ISIiRidGJy1JJWRpZmZHSSpwcm90ZWN0ZWRHRi82JC1JInpHRiY2I0YlRiVGJyEiKSooRiVGKiwmISM4RidGKSIiJUYnLUYuNiRGMS1JIiRHRi82JEYlRipGJ0Y0KiZGJSIiJC1GLjYkRjEtRjw2JEYlRj9GJyIjJyoqJkYlRjgtRi42JEYxLUY8NiRGJUY4RiciIzsqKCwoRidGJ0YlIiIpRilGOEYnLChGJ0YnRiVGNEYpRjhGJ0YxRidGJw==

dsol;

NiMsKiooSSRfQzFHNiIiIiJJInhHRiYjISIiIiIjLUkkZXhwRzYkSSpwcm90ZWN0ZWRHRi9JKF9zeXNsaWJHRiY2I0YoRidGJyooSSRfQzJHRiZGJ0YoRiktRi02IywkRihGKkYnRicqKkkkX0MzR0YmRictSSNFaUdGLjYjLCRGKCEiI0YnRixGJ0YoRilGJyoqSSRfQzRHRiZGJy1GOjYjLCRGKEYrRidGNEYnRihGKUYn

In the theory, "initial conditions" are really first terms of asymptotic expansions. We proceed to set up a linear system to determine the constants NiNJJF9DMUc2Ig==, ..., above.Order:=3;

NiM+SSZPcmRlckc2IiIiJA==

In order to identify NiMtSSVldmFsR0kqcHJvdGVjdGVkR0YlNiQtSSVkaWZmR0YlNiQtJkkiSUc2IjYjSSNudUdGLTYjSSJ4R0YtRi8vRi8qJiIiIkY0IiIjISIi, we will use the MultiSeries package (Meunier, Salvy, and Sedoglavic), which deals with general asymptotic scales and parameterized asymptotics.with(MultiSeries,series);

Warning, the protected name series has been redefined and unprotected

NiM3I0knc2VyaWVzR0kqcHJvdGVjdGVkR0Yl

series(BesselI(nu,x),x);

NiMsKCooLUkmR0FNTUFHNiRJKnByb3RlY3RlZEdGKEkoX3N5c2xpYkc2IjYjLCZJI251R0YqIiIiRi5GLiEiIi1JJGV4cEdGJzYjKiYtSSNsbkdGJzYjIiIjRi5GLUYuRi8pSSJ4R0YqRi1GLkYuKipGLEYvRiVGL0YwRi8pRjksJkYtRi5GN0YuRi4jRi4iIiUtSSJPR0YoNiMpRjksJkY+Ri5GLUYuRi4=

diff(%,nu);

NiMsMioqLUkmR0FNTUFHNiRJKnByb3RlY3RlZEdGKEkoX3N5c2xpYkc2IjYjLCZJI251R0YqIiIiRi5GLiEiIi1JJGV4cEdGJzYjKiYtSSNsbkdGJzYjIiIjRi5GLUYuRi8pSSJ4R0YqRi1GLi1JJFBzaUdGJ0YrRi5GLyoqRiVGL0YwRi9GOEYuRjRGLkYvKipGJUYvRjBGL0Y4Ri4tRjU2I0Y5Ri5GLioqRiwhIiNGJUYvRjBGLylGOSwmRi1GLkY3Ri5GLiNGLyIiJSosRixGL0YlRi9GMEYvRkJGLkY6Ri5GRCosRixGL0YlRi9GMEYvRkJGLkY0Ri5GRCosRixGL0YlRi9GMEYvRkJGLkY+Ri4jRi5GRS1JIk9HRig2IyomKUY5LCZGRUYuRi1GLkYuRj5GLkYu

A truncated asymptotic expansion for NiMtSSVldmFsR0kqcHJvdGVjdGVkR0YlNiQtSSVkaWZmR0YlNiQtJkkiSUc2IjYjSSNudUdGLTYjSSJ4R0YtRi8vRi8qJiIiIkY0IiIjISIi therefore is:fs:=map(simplify,eval(%,nu=1/2));

NiM+SSNmc0c2IiwyKioiIiMjIiIiRihJInhHRiVGKSwoISIjRipJJmdhbW1hR0kqcHJvdGVjdGVkR0YvRiotSSNsbkc2JEYvSShfc3lzbGliR0YlNiNGKEYoRipJI1BpR0YvIyEiIkYoRioqKkY1RjZGKEYpRitGKUYwRipGNyoqRjVGNkYoRilGK0YpLUYxNiNGK0YqRioqKEY1RjZGKEYpRisjIiImRigjRjciIioqKkYoRilGK0Y9RixGKkY1RjYjRioiIicqKkY1RjZGKEYpRitGPUYwRiojRjdGQyoqRjVGNkYoRilGK0Y9RjpGKkZCLUkiT0dGLzYjKiZGKyNGQEYoRjpGKkYq

Returning to the general solution to the 4th-order ODE, we derive a truncated asymptotic expansion for it:series(dsol,x);

NiMsKiooLDIqJkkkX0MxRzYiIiIiLUkjbG5HNiRJKnByb3RlY3RlZEdGLUkoX3N5c2xpYkdGKDYjKiRJInhHRighIiJGMkYpKiZJJF9DMkdGKEYpRipGMkYpKihJJF9DM0dGKEYpSSZnYW1tYUdGLUYpRipGMkYpRjZGMiooRjZGKS1GKzYjIiIjRilGKkYyRikqKEkkX0M0R0YoRilGN0YpRipGMkYpRj1GMiooRj1GKUY5RilGKkYyRilGKUYqRilGMSNGMkY7RikqKCw2RiZGMkYzRilGNUYyRjZGKUY4RjIqJkY2RilGKkYyRjtGPEYpRj1GMkY+RikqJkY9RilGKkYyISIjRilGKkYpRjEjRilGO0YyKigsNkYmRilGM0YpRjVGKUY2RjJGOEYpRkJGREY8RilGPUYyRj5GKUZDRkRGKUYqRilGMSMiIiRGO0ZFLUkiT0dGLTYjKiRGMSMiIiZGO0Yp

dsol_fs:=eval(%,nu=1/2);

NiM+SShkc29sX2ZzRzYiLCoqKCwyKiZJJF9DMUdGJSIiIi1JI2xuRzYkSSpwcm90ZWN0ZWRHRi9JKF9zeXNsaWJHRiU2IyokSSJ4R0YlISIiRjRGKyomSSRfQzJHRiVGK0YsRjRGKyooSSRfQzNHRiVGK0kmZ2FtbWFHRi9GK0YsRjRGK0Y4RjQqKEY4RistRi02IyIiI0YrRixGNEYrKihJJF9DNEdGJUYrRjlGK0YsRjRGK0Y/RjQqKEY/RitGO0YrRixGNEYrRitGLEYrRjMjRjRGPUYrKigsNkYpRjRGNUYrRjdGNEY4RitGOkY0KiZGOEYrRixGNEY9Rj5GK0Y/RjRGQEYrKiZGP0YrRixGNCEiI0YrRixGK0YzI0YrRj1GNCooLDZGKUYrRjVGK0Y3RitGOEY0RjpGK0ZERkZGPkYrRj9GNEZARitGRUZGRitGLEYrRjMjIiIkRj1GRy1JIk9HRi82IyokRjMjIiImRj1GKw==

Identifying the known solution with this general solution yields a linear systemzz:=convert(simplify(2*sqrt(Pi)*sqrt(x)*series(dsol_fs-fs,x)),polynom);

NiM+SSN6ekc2IixcbyomSSNQaUdJKnByb3RlY3RlZEdGKSMiIiIiIiNJJF9DMUdGJUYrRiwqJkYoRipJJF9DMkdGJUYrRiwqKEkieEdGJUYrRihGKkYvRishIiMqKEYxRitGKEYqSSRfQzNHRiVGKyEiJSooRjFGK0YoRipJJF9DNEdGJUYrIiIlKihGMUYrRixGKkkmZ2FtbWFHRilGK0YyKiZGMUYrRixGKkY4KihGKEYqRjdGK0Y6RitGLCooRihGKkY3RistSSNsbkc2JEYpSShfc3lzbGliR0YlNiNGLEYrRiwqKEYoRipGNEYrRjpGK0YsKihGKEYqRjRGK0Y+RitGLCoqRjFGK0YoRipGNEYrRjpGK0YsKipGMUYrRihGKkY0RitGPkYrRiwqKkYxRitGKEYqRjRGKy1GPzYjKiRGMSEiIkYrRjIqKkYxRitGKEYqRjdGK0Y6RitGMioqRjFGK0YoRipGN0YrRkhGK0YsKipGMUYrRihGKkY3RitGPkYrRjIqKkYxRixGKEYqRjRGK0Y6RitGKyoqRjFGLEYoRipGNEYrRkhGK0ZLKipGMUYsRihGKkY0RitGPkYrRisqKkYxRixGKEYqRjdGK0Y6RitGKyoqRjFGLEYoRipGN0YrRkhGK0ZLKipGMUYsRihGKkY3RitGPkYrRisqKEYxRixGKEYqRjdGK0YyKihGKEYqRjRGK0ZIRitGMiooRihGKkY3RitGSEYrRjIqKEYxRitGPkYrRixGKkYyKihGMUYrRixGKkZIRitGLCooRjFGLEYoRipGLUYrRisqKEYxRixGKEYqRi9GK0YrKihGMUYsRihGKkY0RitGMiooRjFGK0YoRipGLUYrRiw=

sys:={coeffs(zz,{x,ln(1/x)})};

NiM+SSRzeXNHNiI8KCwmKiZJI1BpR0kqcHJvdGVjdGVkR0YqIyIiIiIiI0kkX0MzR0YlRiwhIiMqJkYpRitJJF9DNEdGJUYsRi8sJkYwISIiRihGMywoRjBGLSokRi1GK0YtRihGLywuKiZGKUYrSSRfQzFHRiVGLEYtKiZGKUYrSSRfQzJHRiVGLEYtKihGKUYrRi5GLC1JI2xuRzYkRipJKF9zeXNsaWJHRiU2I0YtRixGLSooRilGK0YxRixJJmdhbW1hR0YqRixGLSooRilGK0YxRixGPEYsRi0qKEYpRitGLkYsRkJGLEYtLDhGOUYvRighIiVGMCIiJSomRi1GK0ZCRixGL0Y1RkdGREYtRjtGLSomRjxGLEYtRitGL0ZBRi9GQ0YvRjdGLSwyRkFGLEZERixGQ0YsRjtGLEY3RixGOUYsRihGL0YwRi8=

sol:=solve(sys,{_C1,_C2,_C3,_C4});

NiM+SSRzb2xHNiI8Ji9JJF9DMkdGJSIiIS9JJF9DMUdGJUYpL0kkX0M0R0YlLCQqJiIiIyMiIiJGMEkjUGlHSSpwcm90ZWN0ZWRHRjQjISIiRjBGNS9JJF9DM0dGJSwkRi9GMQ==

Our final expression for NiMtSSVldmFsR0kqcHJvdGVjdGVkR0YlNiQtSSVkaWZmR0YlNiQtJkkiSUc2IjYjSSNudUdGLTYjSSJ4R0YtRi8vRi8qJiIiIkY0IiIjISIiisexpr:=eval(dsol,sol);

NiM+SSVleHByRzYiLCYqLCIiIyMiIiJGKEkjUGlHSSpwcm90ZWN0ZWRHRiwjISIiRigtSSNFaUc2JEYsSShfc3lzbGliR0YlNiMsJEkieEdGJSEiI0YqLUkkZXhwR0YxNiNGNUYqRjVGLUYpKixGKEYpRitGLS1GMDYjLCRGNUYoRiotRjg2IywkRjVGLkYqRjVGLUYt

It is really the announced right-hand side.normal(expr-fo);

NiMiIiE=

(Repeated:)

expr;

NiMsJiosIiIjIyIiIkYlSSNQaUdJKnByb3RlY3RlZEdGKSMhIiJGJS1JI0VpRzYkRilJKF9zeXNsaWJHNiI2IywkSSJ4R0YwISIjRictSSRleHBHRi42I0YzRidGM0YqRiYqLEYlRiZGKEYqLUYtNiMsJEYzRiVGJy1GNjYjLCRGM0YrRidGM0YqRio=

The exponential integrals and logarithms implied in all asymptotic expansions induce branch cuts on the positive real line and negative real line. Of course, the derivation above could be reproduced with adequate changes for NiMySSJ4RzYiIiIh, NiMyIiIhLUkjSW1HSSpwcm90ZWN0ZWRHRic2I0kieEc2Ig==, and NiMyLUkjSW1HSSpwcm90ZWN0ZWRHRiY2I0kieEc2IiIiIQ==, respectively.A uniform treatment of the identity and functions above for a complex argument, taking branch cuts into account, is beyond this session and beyond the current implementations. The topic is the core of Ludovic Meunier's thesis (in preparation).