3
$\begingroup$

Assuming that both $a$ and $b$ are complex and $| b |<1$, $| a |=1$, I want to prove that $\left|\frac{a-b}{1-a^* b}\right|=1$.

My code:

Clear["Global`*"];
Reduce[Abs[(x + I y - (u + I v))/(1 - Conjugate[x + I y]*(u + I v))] ==
    1 && x ∈ Reals && y ∈ Reals && 
  u ∈ Reals && v ∈ Reals && Abs[x + I y] == 1 && 
  Abs[u + I v] < 1, {x, y, u, v}]

$\begin{aligned} & \left(x=-1 \& \& y=\theta \& \&-1<u<1 \& \&-\sqrt{1-u^2}<v<\sqrt{1-u^2}\right)|| \\ & \left(-1<x<1 \& \&\left(\left(y=-\sqrt{1-x^2} \& \&-1<u<1 \& \&-\sqrt{1-u^2}<v<\sqrt{1-u^2}\right)||\left(y=\sqrt{1-x^2} \& \&-1<u<1 \& \&-\sqrt{1-u^2}<v<\sqrt{1-u^2}\right)\right)\right)||\left(x=1 \& \& y=\theta \& \&-1<u<1 \& \&-\sqrt{1-u^2}<v<\sqrt{1-u^2}\right)\end{aligned}$

The answer I want is either True or some other way to simplify $\left|\frac{a-b}{1-a^* b}\right|$ to 1.

$\endgroup$

4 Answers 4

8
$\begingroup$
Clear["Global`*"]

Use ComplexExpand and since the known constraints are in terms of Abs, set TargetFunctions to {Abs, Arg}

Assuming[{Abs[b] < 1 && Abs[a] == 1},
 FullSimplify@
  ComplexExpand[Abs[(a - b)/(1 - Conjugate[a] b)], {a, b}, 
   TargetFunctions -> {Abs, Arg}]]

(* 1 *)
$\endgroup$
4
$\begingroup$
Simplify[
 ExpandAll@
  ComplexExpand[
   Abs[(x + I y - (u + I v))/(1 - Conjugate[x + I y]*(u + I v))]],
 {a, b, u, v} \[Element] Reals && u^2 + v^2 < 1 && x^2 + y^2 == 1]

(*  1  *)

Or:

Reduce[
 Implies[
  u^2 + v^2 < 1 && x^2 + y^2 == 1,
  ComplexExpand[
   Abs[(x + I y - (u + I v))/(1 - Conjugate[x + I y](u + I v))]] == 1
  ],
 {}, Reals]

(*  True  *)
$\endgroup$
4
$\begingroup$

It is really somehow unsettling (at least to me) that Mathematica, being inherently adapted to work with complex numbers, requires one to manually write x + I y instead of just using complex a. One would certainly expect that the following works:

FullSimplify[Abs[(a - b)/(1 - Conjugate[a] b)], 
 Abs[b] < 1 && Abs[a] == 1] 
(* Abs[(-a + b)/(-1 + b Conjugate[a])] *)

yet it returns practically the same result.

However, it seems that we can somehow trick Mathematica into grinding this expression more thoroughly by constructing a custom ComplexityFunction that minimizes the amount of certain "forbidden" functions:

FullSimplify[Abs[(a - b)/(1 - Conjugate[a] b)], 
 Abs[b] < 1 && Abs[a] == 1, 
 ComplexityFunction -> (Count[#, Conjugate[_] | Re[_] | Sign[_], All] &)]
(* 1 *)

I got to this particular choice of functions by brute-force trying different combinations. We can look at possible choices more systematically:

funcs = {Abs[_], Conjugate[_], Re[_], Sign[_]};
alts = Alternatives @@@ Subsets[funcs];
Table[{FullSimplify[Abs[(a - b)/(1 - Conjugate[a] b)], 
    Abs[b] < 1 && Abs[a] == 1, 
    ComplexityFunction -> (Count[#, alt, All] &)], alt}, {alt, alts}] // Grid

enter image description here

It seems that only Conjugate[_] | Re[_] | Sign[_] works. One step further, we can combine it also with LeafCount:

Table[{FullSimplify[Abs[(a - b)/(1 - Conjugate[a] b)], 
    Abs[b] < 1 && Abs[a] == 1, 
    ComplexityFunction -> (LeafCount[#] + 10 Count[#, alt, All] &)], 
   alt}, {alt, alts}] // Grid

enter image description here

Therefore, combining LeafCount with the number of Conjugates (weighted more heavily by some small factor) also works:

FullSimplify[Abs[(a - b)/(1 - Conjugate[a] b)], 
 Abs[b] < 1 && Abs[a] == 1, 
 ComplexityFunction -> (LeafCount[#] + 5 Count[#, Conjugate[_], All] &)]
(* 1 *)
$\endgroup$
3
$\begingroup$

b can be any complex number except $a^*b=1\iff a=b$, assuming, therefore, $a\neq b$:

enter image description here

Here is a Mathematica verification:

a = Cos [t] + I Sin[t];
b= x+ I y;
f= (a -b) / (1 - Conjugate [a]b);
FullSimplify[f Conjugate [f], t\[Element] Reals]

yields 1. So square of modulus is 1, modulus is 1.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.