I am trying to simplify the expression
1/2 * log(2) - 1/2 * log(2 * x + 2 * sqrt(x^2 - 1))
under the assumptions that x is real, and x > 1. I expect
1/2 * acosh(x)
I tried
with assuming(s, x, 'real', x > 1):
print(integrate(sqrt(abs(1 - s * s)), s, 1, x).full_simplify())
However, that just prints back the original expression.
I would do this by hand as follows:
$$ \begin{aligned} {} & 1/2 * \log(2) - 1/2\log(2 * x + 2\sqrt{x^2 - 1}) \\ = & 1/2 * \log(2) - 1/2\log(2 * (x + \sqrt{x^2 - 1})) \\ = & 1/2 * \log(2) - 1/2\log(2) - 1/2\log(x + \sqrt{x^2 - 1}) \\ = & 1/2\log(x + \sqrt{x^2 - 1}) \\ = & 1/2* \textrm{acosh}(x) \\ \end{aligned} $$
How can I get SageMath to perform this simplification?