# Prove that the modulus of a complex function is 1

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

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

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 *)

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  *)


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


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


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 *)


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

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.