Prove $\int_0^{\infty}{\frac{1}{e^{sx}\sqrt{1+s^2}}}ds < \arctan\left(\frac1x\right),\quad\forall x\ge1$

Here is a proof of the inequality for $x\geq 2$. For the remaining range, see the Added section below.

Let $\lambda:=1-1/\sqrt{2}$, then by convexity we have $$\frac{1}{\sqrt{1+s^2}}\leq 1-\lambda s^2,\qquad 0\leq s\leq 1.$$ Using this bound we can estimate \begin{align*}\int_0^{\infty}{\frac{1}{e^{sx}\sqrt{1+s^2}}}\,ds&<\int_0^1\frac{1-\lambda s^2}{e^{sx}}\,ds+\int_1^\infty\frac{1-\lambda}{e^{sx}}\,ds\\[6pt] &=\frac{1}{x}-\lambda\left(\int_0^1\frac{s^2}{e^{sx}}\,ds+\int_1^\infty\frac{1}{e^{sx}}\,ds\right)\\[6pt] &=\frac{1}{x}-2\lambda\frac{1-e^{-x}x-e^{-x}}{x^3} .\end{align*} On the other hand, for $x>0$ we also have $$\arctan\left(\frac{1}{x}\right)=\int_0^{1/x}\frac{1}{1+s^2}\,ds>\int_0^{1/x}(1-s^2)\,ds=\frac{1}{x}-\frac{1}{3x^3},$$ hence it suffices to verify that $$\lambda(1-e^{-x}x-e^{-x})>\frac{1}{6},\qquad x\geq 2.$$ This is straightforward, so we proved the original inequality for $x\geq 2$.

Added. One can cover the remaining range $1\leq x<2$ as follows. Let $f(x)$ denote the LHS and $g(x)$ denote the RHS in the original inequality. These two functions are decreasing, hence it suffices to verify the following $20$ numeric inequalities: $$f(1+(n-1)/20)<g(1+n/20),\qquad n=1,2,\dots,20.$$ These are likely to be true, e.g. I checked them with Mathematica's NIntegrate command.


The inequality holds by direct calculation for $x$ close to unity, when the two sides are well separated, but for large $x$ the two sides approach each other and we need to check that the inequality is not violated.

I denote $x\equiv 1/\epsilon$, and seek to prove that $$\int_0^{\infty}{\frac{\epsilon}{e^{s}\sqrt{1+\epsilon^2 s^2}}}ds < \arctan\epsilon,\;\;0<\epsilon\leq 1.$$ Series expansion of both sides gives $$\int_0^{\infty}{\frac{\epsilon}{e^{s}\sqrt{1+\epsilon^2 s^2}}}ds=\epsilon-\epsilon^3+{\cal O}(\epsilon^5),$$ $$\arctan\epsilon=\epsilon-\tfrac{1}{3}\epsilon^3+{\cal O}(\epsilon^5).$$ This proves the inequality for $\epsilon$ close to $0$, hence for large $x$.