For $0 \leq a_n, b_n$: Is $\varliminf a_n \varlimsup b_n \leq \varlimsup a_n b_n $ true? The sequences are assumed to be bounded!
I suspect it is, since $\varliminf a_n + \varlimsup b_n \leq \varlimsup (a_n+b_n)$ is. But I have not managed to prove it.
I thought it possible to mirror the following trick when proving the inequality for sums:

$\varlimsup b_n = \varlimsup (a_n + b_n - a_n) \leq \varlimsup (a_n + b_n ) + \varlimsup(-a_n) = \varlimsup (a_n + b_n )  -\varliminf(a_n)$

But the incipient idea fell short rather fast:

$0 = \varlimsup (a_n b_n - a_n b_n) \leq  \varlimsup (a_n b_n) + \varlimsup (-a_n b_n)$

I was hoping to manipulate $\varlimsup (-a_n b_n)$ in some ingenious way, but have not succeded.
Would love to read any ideas or hints.
 A: Under the assumption that the sequences $(a_n)$ and $(b_n)$ are bounded:
Let $\alpha = \liminf a_n$ and $\beta = \limsup b_n$ (the boundedness assumption telling us that $-\infty < \alpha,\beta < \infty)$.  Let $\epsilon > 0$.  By definitions, we know that $a_n > \alpha - \epsilon$ for all $n$ sufficiently large and that $b_n > \beta - \epsilon$ for infinitely many $n$.  Therefore also $a_n b_n > (\alpha - \epsilon)(\beta - \epsilon) = \alpha\beta - \epsilon(\alpha+\beta) + \epsilon^2$ for infinitely many $n$.  This implies that $\limsup (a_n b_n) > \alpha\beta - \epsilon(\alpha+\beta) + \epsilon^2$.  This holds for arbitrary $\epsilon$, so we conclude $\limsup(a_n b_n) \geq \alpha \beta$ as desired.
If either of the sequences is not bounded, there may be some other cases to check, but I am a bit too lazy to check them all :)
A: The fact that the exponential function is continuous and increasing implies that liminfs and limsups pass through the exponential function. Setting $a_n=e^{A_n} ,\ b_n= e^{B_n}$ this turns the inequality into $$\exp(\liminf A_n + \limsup B_n) \le \exp(\limsup (A_n + B_n))$$ Since the exponential function is increasing we can cancel it on both sides which reduces it to the additive known result. Since this result is true for bounded sequences (including negative values), we are done.
