Определенный интеграл

[nikov]

Результаты численного интегрирования позволяют предположить, что

$$\int_0^{\infty}x^3\,\text{Ci}(x)\,\text{li}\left(e^{-x}\right)\,dx=\frac{3\ln 2}{2}-\frac{5}{4},$$

где

$$\text{Ci}(x)=-\int_x^{\infty}\frac{\cos t}{t}\,dt,\,\text{li}(x)=\int_0^x\frac{1}{\ln t}\,dt.$$

Но у меня пока не получается это доказать (или опровергнуть ). Mathematica 8 / WolframAlpha тоже не справляются с этим примером. Есть ли у кого-нибудь идеи на этот счёт?

P.S. Есть ли какие-то известные примеры определённых интегралов, для которых нет доказанного выражения в замкнутой форме, хотя и есть предположительное выражение, подтверждаемое численным интегрированием?

[sup]

Судя по всему, этот интеграл берется по частям. Систематически перебрасываем производные на те "гадкие" функции. В результате - произведение степени, экспоненты и косинуса.

[Slip]

nikov,

ответ действительно такой. берется по частям - сначала куб под дифференциал, получаются два интеграла, в каждом из которых уже только одна интегральная функция, их еще раз по частям( правда, тут уже просто по частям нельзя, нужно аккуратно расписать, что будет происходить в окрестности нуля ). В результате каждый из последних двух интегралов будет равен сумме двух - один вида сумма произведений косинусов, синусов, экспонент и степеней, а другой - $\int\limits_0^{+\infty}e^{-x}\frac{\cos x-1}x\, dx$ или $\int\limits_0^{+\infty}\cos x\frac{1-e^{-x}}x\, dx$. Последние два легко берутся введением параметра и дифференцированием по нему.

З.Ы. Иногда полезно посчитать что-нибудь такое нудное на ночь ;)

[Aleksandrito]

Вы не хотите попробовать Представления:
$Ci(x)=C-ln(x)+\sum_{\infty }^{k=1}(-1)^k\cdot \frac{x^{2k}}{2k(2k)!}$;
$li(x)=Ei(ln(x));$, где Ei - интегральная показательная функция, терпящая разрыв в 1 интегрируется в пределах $(0;1-\varepsilon )(1+\varepsilon ;\infty )$, где $\varepsilon $ - бесконечно малая первого порядка;
$ С=0,5772156649$ - постоянная Эйлера;
И проинтегрировать ?