84
$\begingroup$

The following identity on MathSE

$$\int_0^{1}\arctan\left(\frac{\mathrm{arctanh}\ x-\arctan{x}}{\pi+\mathrm{arctanh}\ x-\arctan{x}}\right)\frac{dx}{x}=\frac{\pi}{8}\log\frac{\pi^2}{8}$$

seems to be very difficult to prove.

Question: I worked on this identity for several days without any success. Is there any clue how to prove this integral identity?

Improve this question
$\endgroup$
8
  • 15
    $\begingroup$ I'm waiting for Noam Elkies's solution :-) $\endgroup$
    – Suvrit
    Commented Jan 18, 2014 at 19:20
  • 2
    $\begingroup$ A related problem can be found here. $\endgroup$
    – Lucian
    Commented Jan 21, 2014 at 15:08
  • 4
    $\begingroup$ What happens if $\pi$ in the integral is replaced by some other real number? Can one give a closed-form formula for the integral in this case? $\endgroup$
    – Zurab Silagadze
    Commented Jan 23, 2014 at 5:32
  • 16
    $\begingroup$ Where does this problem come from and why do you care about it? $\endgroup$
    – Lev Borisov
    Commented Jan 24, 2014 at 3:46
  • 6
    $\begingroup$ @LevBorisov: This identity is a long-lasting problem(which was raised by another user) on Math.SE, and I think it is just the type of identity which may appear in Ramanujan's notebooks. Although I don't know what this identity may related to, it would be better to draw more attention to this elegent identity. $\endgroup$
    – Y. Zhao
    Commented Jan 28, 2014 at 12:15

1 Answer 1

Reset to default
94
+150
$\begingroup$

I have proved this equality by means of Cauchy’s Theorem applied to an adequate function. Since my solution is too long to post it here, I posted it in arXiv:

  • Juan Arias de Reyna, Computation of a Definite Integral, arXiv:1402.3830.

The function $$G(z)=\frac{\log(1+(1+i)\,f(z)\,)}z$$ where $$f(x)=\frac{\operatorname{arctanh}(x)-\arctan(x)}{\pi}$$ extended analytically.

Improve this answer
$\endgroup$
4
  • $\begingroup$ That's great. I suggest that you at least copy the definitions of the key functions $f(z)$ and $G(z)$ into your answer. $\endgroup$
    – Neil Strickland
    Commented Feb 18, 2014 at 8:57
  • 1
    $\begingroup$ @larry, I would like to know how this question was generated. I have seen so much structure in your integrand that I will be surprised if there is not something hidden. $\endgroup$
    – juan
    Commented Feb 18, 2014 at 9:49
  • 1
    $\begingroup$ Nice observation! Thanks for your answer to this identity! $\endgroup$
    – Y. Zhao
    Commented Feb 19, 2014 at 14:42
  • 5
    $\begingroup$ Awesome answer! --- it's more than just an observation, I'd say :-) $\endgroup$
    – Suvrit
    Commented Feb 19, 2014 at 16:32

You must log in to answer this question.

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