Algorithmic simplification of expressions with $\arctan$, e.g. $2\arctan\frac{5-\sqrt2}{5+\sqrt2}=3\arctan\frac{1}{2\sqrt2}$.
This is a problem I encountered in another (unrelated) question.
I got an expression which is a bit ugly, $2\arctan\frac{5-\sqrt2}{5+\sqrt2}$, but when changing the method I got another prettier expression, $3\arctan\frac{1}{2\sqrt2}$.
Since they are both equal to the same integral, they must be equal as well (and we can easily prove that by doing some simple calculation). But what makes it interesting is, a lot of common mathematics software cannot do this kind of simplification (I tried SageMath and WolframAlpha, they both did nothing).
So let's do it by hand to see what happened.
\begin{align} 2\arctan\frac{5-\sqrt2}{5+\sqrt2} &= \arctan\frac{23}{10\sqrt2}\tag{automatic}\\ &= \arg\left(10\sqrt2+23i\right)\tag{automatic}\\ &= \arg\left(2\sqrt2+i\right)^3\tag{miracle}\\ &= 3\arctan\frac{1}{2\sqrt2}.\tag{automatic} \end{align}
(In the general case, we should also count how many $\pi$ should be added at the end.)
As you can see, the key step here is the factorization $10\sqrt2+23i=\left(2\sqrt2+i\right)^3$. This is a factorization in $\mathbb Z[\sqrt2,i]$, which might be difficult even for computers (I'm not sure).
What's more, normally there's not just $\sqrt2$ that appears, e.g. $$\arctan\frac{\sqrt5-77\sqrt2}{7+11\sqrt{10}}=3\arctan\sqrt5+5\arctan\sqrt2-3\pi.$$
So here is my question:
Is there an algorithmic way to do this kind of simplification?
Let me explain a little where this problem comes from.
I got an integral, for $a>0$:
$$\int_0^\infty e^{-at}\left(\operatorname{erf}\sqrt t\right)^3\,dt=\frac{4}{\pi}\frac1{a\sqrt{a+1}}\arctan\frac{1-b}{1+b},$$
where $b=\frac{a}{a+4}\sqrt{\frac{a+3}{a+1}}$.
I wanted to simplify this expression but failed. The example mentioned before is just the case $a=1$.
I'd be glad if anyone can simplify this expression for any $a>0$, and I'll take it as an acceptable answer since I think this expression is already complicated enough.
I added my answer to the integral problem only.
$$\int_0^\infty e^{-at}\left(\operatorname{erf}\sqrt t\right)^3\,dt=\frac{12}{\pi}\frac1{a\sqrt{a+1}}\left(\arctan\sqrt{\frac{a+3}{a+1}}-\frac\pi4\right).$$
And it didn't give us a general method to deal with all cases.
As you noted, this question is equivalent to factoring numbers in the ring $\mathbb Z[\sqrt2,i]$. I don't know whether or not unique factorization holds here, even though it does in $\mathbb Z[\sqrt 2]$ and $\mathbb Z[i]$. If it does not we may have many ways of writing a number as a product of irreducible elements, and some might be more interesting than others. Another complication is that this ring has infinitely many units which are related to the solutions of the Pell equation $x^2-2y^2=\pm 1$. It is possible to do this, but it's violent and terrible. As an appetizer have the identity:
$$2\sqrt 2+i=-i(1+i\sqrt 2)^2$$
$$\arctan\left(\frac 1{2\sqrt 2}\right)=2\arctan(\sqrt 2)-\frac\pi 2$$
Consider a general number in our ring
$$x_1=a+b\sqrt 2+ci+di\sqrt 2$$
Its algebraic conjugates are:
$$x_2=a-b\sqrt 2+ci-di\sqrt 2$$
$$x_3=a+b\sqrt 2-ci-di\sqrt 2$$
$$x_4=a-b\sqrt 2-ci+di\sqrt 2$$
And define the norm
$$N(x_1)=x_1x_2x_3x_4=a^4 - 4a^2b^2 + 2a^2c^2 + 4a^2d^2 - abcd + 4b^4 + 4b^2c^2 + 8b^2d^2 + c^4 - 4c^2d^2 + 4d^4$$
By grouping the quartet of conjugates two by two and applying the definition we also get
\begin{align*} N(x_1)=(x_1x_3)(x_2x_4)&=(a^2+2b^2+c^2+2d^2+(2ab+2cd)\sqrt 2)(a^2+2b^2+c^2+2d^2-(2ab+2cd)\sqrt 2)\\ &=(a^2+2b^2+c^2+2d^2)^2-2(2ab+2cd)^2 \end{align*}
And also
\begin{align*} N(x_1)=(x_1x_2)(x_3x_4)&=(a^2-2b^2-c^2+2d^2+(2ac-4bd)i)(a^2-2b^2-c^2+2d^2-(2ac-4bd)i) \\ &=(a^2-2b^2-c^2+2d^2)^2+(2ac-4bd)^2 \end{align*}
So we immediately get that the norm of any element is the sum of two squares (at least one even) and also a square minus twice a square. We start with
$$N(5+\sqrt 2+5i-i\sqrt 2)=2916=2^2 3^6$$
By putting the leading $2$ into the arctangent you effectively square this number, which makes things harder even though there's some cancelation
$$N(10\sqrt 2+23i)=531441=3^{12}$$
Since any number must have a norm which is the sum of two squares at least one of which must be even, it's easy to see that none has norm 2 or 3. Here's a search for elements with norm 9 with c++
const constexpr double sqrt2 = std::sqrt(2);
const constexpr std::complex<double> half = (0.5,0.0);
for(int a = 0; a != 201; ++a) {
for(int b = 0; b != 201; ++b) {
for(int c = 0; c != 201; ++c) {
for(int d = 0; d != 201; ++d) {
std::complex<double> x1 (a+b*sqrt(2), c+d*sqrt(2));
std::complex<double> x2 (a-b*sqrt(2), c-d*sqrt(2));
std::complex<double> x3 (a+b*sqrt(2),-c-d*sqrt(2));
std::complex<double> x4 (a-b*sqrt(2),-c+d*sqrt(2));
auto prod = x1 * x2 * x3 * x4 + half;
int n = prod.real();
if(n == 9) std::cout << a << " " << b << " " << c << " " << d << "\n";
}
}
}
}
I ran this both 4 and 9 to find the following. This is the output for 4. I chose to try $1+i$ first because it's the simplest looking one, and it was a success
$$5+\sqrt 2+5i-i\sqrt 2=(1+i)(5-i\sqrt 2)$$
When trying the next step the first try fails because $5-i\sqrt 2$ is not a multiple of $\sqrt 2+i$, but the next one succeeds
$$5+\sqrt 2+5i-i\sqrt 2=(1+i)(1+i\sqrt 2)(1-2i\sqrt 2)$$
It works thrice in fact
$$5+\sqrt 2+5i-i\sqrt 2=-(1+i)(1+i\sqrt 2)^3$$
Which corresponds to
$$\arctan\left(\frac{5-\sqrt 2}{5+\sqrt 2}\right)=3\arctan(\sqrt 2)-\frac {3\pi}4$$
Just an answer to what I edited after.
For $a>0$, let
$$b(a)=\frac{a}{a+4}\sqrt{\frac{a+3}{a+1}},$$ $$f(a) = \arctan\frac{1-b(a)}{1+b(a)}.$$
Then,
$$f'(a) = -\frac{3}{2 \, {\left(a + 2\right)} {\left(a + 1\right)}}\sqrt{\frac{a+1}{a+3}},$$ $$\int f'(a)\,da =3\arctan\sqrt{\frac{a+3}{a+1}} + Const,$$
and here we have $Const = -\frac34\pi$. Thus, for $a>0$,
$$\int_0^\infty e^{-at}\left(\operatorname{erf}\sqrt t\right)^3\,dt=\frac{12}{\pi}\frac1{a\sqrt{a+1}}\left(\arctan\sqrt{\frac{a+3}{a+1}}-\frac\pi4\right).$$