Symbolically prove that two expressions are identical

Question

I encountered this problem when trying to reproduce the result of this paper. (The relevant parts are all included in the preview i.e. the 1st page of the article. This link is just given as background information, the following question is still self-contained without it.)

I want to prove int == intpaper assuming l > 0, τ > 0 where

int = 
  Sqrt[3] (-(1/((Sqrt[-3 + 2 Sqrt[3]] l - I Sqrt[6 - 2 Sqrt[3]] τ) 
      Sqrt[1 + 3/(Sqrt[-3 + 2 Sqrt[3]] l - I Sqrt[6 - 2 Sqrt[3]] τ)^2])) - 
    1/((Sqrt[-3 + 2 Sqrt[3]] l + I Sqrt[6 - 2 Sqrt[3]] τ) 
      Sqrt[1 + 3/(Sqrt[-3 + 2 Sqrt[3]] l + I Sqrt[6 - 2 Sqrt[3]] τ)^2]));

intpaper = Im[2/Sqrt[-1 - (Sqrt[-1 + Sqrt[3]] l - 2 I τ)^2/(3 + Sqrt[3])]];

It's easy to verify their equivalence numerically.

Block[{l, τ}, {l, τ} = RandomReal[1, 2]; intpaper == int]

always returns True. But I don't know how to verify it symbolically. I tried

Simplify[int == intpaper, {l > 0, τ > 0}]

but it was returned unevaluated.

jjstankowicz · Answer

This solution gets a trivial step away from the answer.
(Strikeout after addressing the comments.)

You can consider the difference diff = int - intpaper, and check that it vanishes.

Rather than having Mathematica take the imaginary part, do it "by hand":

intpaperz = 
2/Sqrt[-1 - (Sqrt[-1 + Sqrt[3]] l - 2 I [Tau])^2/(3 + Sqrt[3])];
intpaperzc = 
2/Sqrt[-1 - (Sqrt[-1 + Sqrt[3]] l + 2 I [Tau])^2/(3 + Sqrt[3])];
intpaper = 1/(2 I) (intpaperz - intpaperzc);

which uses $textrm{Im}(z) = (z-z^*)/(2i)$. Note: I assume $tau$ and $l$ are real.

By inspection of the  the resulting expression for diff:

a good change of variables appears to be

$$a = sqrt{6-2sqrt{3}} tau , quad b = l sqrt{-3 + 2sqrt{3}} ,$$

which can be implemeneted by:

out = FullSimplify[
  diff /. {[Tau] -> a/Sqrt[6 - 2 Sqrt[3]], 
    l -> b/Sqrt[-3 + 2 Sqrt[3]]}]

The resulting expression is

This suggests another change of variables:

out = out /. {a + I b -> w, a - I b -> wc, -I a + b -> -I w, I a + b -> I wc};
FullSimplify[out]

This is the trivial last step that I stopped fighting Mathematica on. 
For a complex number (such as w and wc), it's true that $sqrt{w^2} = w$, so both terms vanish.
This last step is not so trivial. As @xzczd pointed out in the comment, this only vanishes if $textrm{Re}(w)>0$ and $textrm{Re}(w^*)> 0$. Well,

$$textrm{Re}(w) = a = sqrt{6-2sqrt{3}} tau $$

and

$$textrm{Re}(w^*) = a ,$$
so I guess $tauge 0$ in the original problem statement.

In Mathematica:

FullSimplify[out,{Re@w > 0, Re@wc > 0}];
(* 0 *)

yarchik · Answer

My solution is in the experimental mathematics style:

Series[int - intpaper, {τ, [Infinity], 12}] // Normal // FullSimplify
(* 0 *)

You have to believe that if two series expansions are equal up to 12th order this is an identity. Advantage of the approach is its unbeatable simplicity. Of course, sceptics with faster computers can verify even higher orders. However, it can never be made fully rigorous, but what is verity after all?

Symbolically prove that two expressions are identical

2 Answers

Add your own answers!

Ask a Question