Proving that $~\sum\limits_{k=2}^{\infty}\frac{(-1)^k}{k^2}~H_k~H_{k-1}=\frac{3}{16}~\zeta(4)$

This is an opportunity to make a tribute to Pieter J. de Doelder (1919-1994) from Eindhoven University of Technology, who evaluated in closed form the given series in a somewhat famous paper (p. 132-133 2.3) (1991). One may start by using the following identity coming from the Cauchy product, $$ \ln^2(1+x) =2\sum_{n=1}^\infty (-1)^{n-1} \frac{H_n}{n+1} \:x^{n+1} $$ giving $$ \int_0^1\frac{\ln(1-x)\ln^2(1+x)}{x} \:dx=2\sum_{n=1}^\infty (-1)^{n-1} \frac{H_n}{n+1} \:\int_0^1 x^{n}\ln(1-x)\:dx, $$ then using the standard evaluation $$ \int_0^1 x^{n}\ln(1-x)\:dx =-\frac{H_{n+1}}{n+1},\quad n\ge0, $$ one gets

$$ \int_0^1\frac{\ln(1-x)\ln^2(1+x)}{x}\:dx=2\sum\limits_{n=2}^{\infty} (-1)^{n-1} \frac{H_n H_{n-1}}{n^{2}}. \tag1 $$

Here are the main steps which de Doelder took to evaluate the related integral.

We clearly have $$ \begin{align} \int_0^1\ln^3\left(\frac{1+x}{1-x}\right)\:\frac{dx}{x}&=\int_0^1\frac{\ln^3\left(1+x\right)}{x}\:dx-3\int_0^1\frac{\ln(1-x)\ln^2(1+x)}{x}\:dx \\\\&+3\int_0^1\frac{\ln^2(1-x)\ln(1+x)}{x}\:dx-\int_0^1\frac{\ln^3\left(1-x\right)}{x}\:dx \end{align} $$ and $$ \begin{align} \int_0^1\frac{\ln^3\left(1-x^2\right)}{x}\:dx&=\int_0^1\frac{\ln^3\left(1+x\right)}{x}\:dx+3\int_0^1\frac{\ln(1-x)\ln^2(1+x)}{x}\:dx \\\\&+3\int_0^1\frac{\ln^2(1-x)\ln(1+x)}{x}\:dx+\int_0^1\frac{\ln^3\left(1-x\right)}{x}\:dx, \end{align} $$ substracting the two equalities, $$ \begin{align} 6\!\!\int_0^1\!\frac{\ln(1-x)\ln^2(1+x)}{x}dx&=\!\int_0^1\!\frac{\ln^3\left(1-x^2\right)}{x}dx-\!\int_0^1\!\!\ln^3\left(\frac{1+x}{1-x}\right)\frac{dx}{x}-2\!\int_0^1\!\frac{\ln^3\left(1-x\right)}{x}dx \\\\&=I_1-I_2-2I_3. \end{align} $$ It is easy to obtain $$ \begin{align} I_1=\int_0^1\!\frac{\ln^3\left(1-x^2\right)}{x}dx&=\frac12 \int_0^1\!\frac{\ln^3\left(1-u\right)}{u}du \quad (u=x^2) \\&=\frac12 \int_0^1\!\frac{\ln^3 v}{1-v}dv \quad (v=1-u) \\&=\frac12 \sum_{n=0}^\infty \int_0^1\!v^n\ln^3 v\:dv \\&=-3\sum_{n=1}^\infty \frac1{n^4} \\&=-\frac{\pi^4}{30}, \end{align} $$ similarly $$ \begin{align} I_3=\int_0^1\!\frac{\ln^3\left(1-x\right)}{x}dx=-\frac{\pi^4}{15}. \end{align} $$ By the change of variable, $ u=\dfrac{1-x}{1+x}$, one has $\dfrac{dx}{x}=\dfrac{-2\:du}{1-u^2}$ getting $$ \begin{align} I_2=\int_0^1\!\!\ln^3\left(\frac{1+x}{1-x}\right)\frac{dx}{x}&=-2\int_0^1\!\frac{\ln^3 u}{1-u^2}du \\&=-2\sum_{n=0}^\infty \int_0^1\!u^{2n}\ln^3u\:dv \\&=12\sum_{n=0}^\infty \frac1{(2n+1)^4} \\&=\frac{\pi^4}{8}. \end{align} $$ Then,

$$ \int_0^1\frac{\ln(1-x)\ln^2(1+x)}{x}\:dx=-\frac{\pi^4}{240} \tag2 $$

and

$$ \sum\limits_{n=2}^{\infty} (-1)^{n} \frac{H_n H_{n-1}}{n^{2}}= \frac{3}{16}\zeta(4)=\frac{\pi^4}{480},\tag3 $$

as announced.

Although I have seen too few proofs in this field to be able to compare, this approach might be interesting.

We transform the sum to a fourfold integral which Mathematica can solve immediately. I hope it should be possible to solve the integral "mathematically" as well, which would then complete the proof.

We have to calculate

$$s=\sum _{k=2}^{\infty } \frac{(-1)^k}{k^2} H(k) H(k-1) $$

Writing

$$\frac{1}{n^2}=\int_0^1 \frac{1}{x}\,dx \int_0^x y^{n-1} \, dy $$

$$\frac{1}{n}=\int_0^1 r^{n-1} \, dr$$

and

$$H(k)=\sum _{n=1}^k \frac{1}{n}=\int_0^1 \left(\sum _{n=1}^k r^{n-1}\right) \, dr=\int_0^1 \frac{1-r^k}{1-r} \, dr$$

the sum $s$ below the integrals becomes

$$si=\frac{1}{x(1-r)(1-s)}\sum _{k=2}^{\infty } (-1)^k \left(1-r^k\right) \left(1-s^{k-1}\right) y^{k-1}$$

Which evaluates to

$$si = \frac{y \left(r^2 s^2 y+r^2 s-r^2 y-r^2-r s^2 y+r y-s+1\right)}{(1-r) (1-s) x (y+1) (r y+1) (s y+1) (r s y+1)}$$

Now the integral to be evaluated is

$$s4 = \int _0^1 dx\int _0^x dy\int _0^1 dr\int _0^1 ds \; si$$

Mathematica finds immediately

$$s4 = \frac{\pi ^4}{480} $$

Since

$$\zeta (4)=\frac{\pi ^4}{90}$$

and

$$\frac{90}{480} = \frac{3}{16} $$

we have finally

$$s = \frac{3}{16} \zeta(4)$$