4
$\begingroup$

Found with Desmos. Claim

$$\int_{-\infty}^{0}\left(\cosh\left(x\right)-1\right)^{x}dx<\pi$$



I cannot show it currently and before I tried the Van der Corput inequality:

Let $x,y>0$ then:

$$|\cosh(x)-\cosh(y)|\geq|x-y|\sqrt{\sinh(x)\sinh(y)}.$$

A proof can be found here An inequality due to Van der Corput

Unforntunately it's really not sufficient and bad because we work on the negative axis.


Edit :

Another attempt wich fails : With the Gary'substitution and :

Let $x>0$ then :

$$\sinh(x)\frac{1}{x}<\cosh(x)$$

Unfortunately the integral below (see comment Gary) converges if we use the lower bound above but it's greater than $\pi$ .


How to show the claim?

Thanks.

Ps: The inequality is not tight.

$\endgroup$
2
  • $\begingroup$ With a change of integration variable you can make it an integral along the positive axis: $$ \int_0^{ + \infty } {\frac{{dx}}{{(\cosh x - 1)^x }}} . $$ However, the Van der Corput inequality is trivial when $y=0$. $\endgroup$
    – Gary
    Aug 29, 2021 at 14:47
  • $\begingroup$ @Gary oh well...Have you an idea to tackle it ? $\endgroup$ Aug 29, 2021 at 14:55

1 Answer 1

5
+50
$\begingroup$

Remark: Although we get a closed-form bound (in terms of elementary functions), the solution is still quite complicated.


We have $$\int_{-\infty}^0 (\cosh x - 1)^x\, \mathrm{d}x = \int_0^\infty 2^{-x}\left(\sinh\frac{x}{2}\right)^{-2x}\,\mathrm{d} x = \int_0^\infty 2^{1 - 2x}(\sinh x)^{-4x}\, \mathrm{d}x.$$


Fact 1: $\int (\sinh x)^{-5}\, \mathrm{d}x = -\frac{\cosh x}{4\sinh^4 x} + \frac{3\cosh x}{8\sinh^2 x} - \frac{3}{8}\ln\frac{\mathrm{e}^x + 1}{\mathrm{e}^x - 1} + C$.

Fact 2: $\int (\sinh x)^{-4}\, \mathrm{d}x = -\frac{\cosh x}{3\sinh^3 x} + \frac{2\cosh x}{3\sinh x} + C$.

Fact 3: $\sinh x \ge x + \frac16 x^3$ for all $x\in [0, 1]$.

Let $T(f(x),a,n)$ denote the $n$-th order Taylor approximation of $f(x)$ at $x = a$.

Fact 4: For all $x\in [0, 1]$, $(1 + x^2/6)^{-4x} \le T((1 + x^2/6)^{-4x}, 0, 12)$.
(Proof: Take logarithm, then take derivative and the 2nd derivative.)

Fact 5: For all $x\in [0, 1]$, $2^{-2x} \le T(2^{-2x}, 0, 6)$.
(Proof: Take logarithm, then take derivative.)

Fact 6: For all $u \in [-1, 0]$, $\mathrm{e}^{-4u} \le T(\mathrm{e}^{-4u}, 0, 8) + \frac{512}{315}u^8$.
(Proof: Take logarithm, then take derivative.)


First, using Fact 1, we have \begin{align*} \int_{5/4}^\infty 2^{1 - 2x}(\sinh x)^{-4x}\, \mathrm{d}x &\le \int_{5/4}^\infty 2^{1 - 2\cdot \frac{5}{4}}(\sinh x)^{-4\cdot \frac{5}{4}}\, \mathrm{d}x \\ &= -\frac{\sqrt2}{4}\left(-\frac{\cosh (5/4)}{4\sinh^4 (5/4)} + \frac{3\cosh (5/4)}{8\sinh^2 (5/4)} - \frac{3}{8}\ln\frac{\mathrm{e}^{5/4} + 1}{\mathrm{e}^{5/4} - 1}\right)\\ &< \frac{3}{500}. \end{align*}

Second, using Fact 2, we have \begin{align*} \int_1^{5/4} 2^{1 - 2x}(\sinh x)^{-4x}\, \mathrm{d}x &\le \int_1^{5/4} 2^{1 - 2\cdot 1}(\sinh x)^{-4\cdot 1}\, \mathrm{d}x\\ &= -\frac{\cosh (5/4)}{6\sinh^3 (5/4)} + \frac{\cosh (5/4)}{3\sinh (5/4)} - \left(-\frac{\cosh 1}{6\sinh^3 1} + \frac{\cosh 1}{3\sinh 1}\right)\\ &< \frac{3}{80}. \end{align*}

Third, using Facts 3-6, we have \begin{align*} &\int_0^1 2^{1 - 2x}(\sinh x)^{-4x}\, \mathrm{d}x\\ \le\,& \int_0^1 2^{1 - 2x}(x + x^3/6)^{-4x}\, \mathrm{d}x\\ =\, & \int_0^1 2^{1 - 2x}(1 + x^2/6)^{-4x}x^{-4x}\, \mathrm{d}x\\ \le\, & 2\int_0^1 T(2^{-2x}, 0, 6) \, T((1 + x^2/6)^{-4x}, 0, 12) \, \left[T(\mathrm{e}^{-4u}, 0, 8) + \frac{512}{315}u^8\right]_{u = x\ln x}\, \mathrm{d} x \tag{1}\\ <\, & 1549/500. \end{align*} Note: The integral in (1) admits a closed form $a_0 + a_1\ln 2 + a_2\ln^2 2 + a_3\ln^3 2 + a_4\ln^4 2 + a_5\ln^5 2 + a_6\ln^6 2$ where $a_i$'s are all rational numbers.

Thus, we have $\int_0^\infty 2^{1 - 2x}(\sinh x)^{-4x}\, \mathrm{d}x < \frac{3}{500} + \frac{3}{80} + 1549/500 < \pi$.

We are done.

$\endgroup$
2
  • $\begingroup$ Impressive ! Let me the time to read it ! $\endgroup$ Sep 2, 2021 at 14:45
  • $\begingroup$ @ErikSatie It is not a nice proof. I hope to see nice proofs. $\endgroup$
    – River Li
    Sep 2, 2021 at 15:24

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .