Talk:Absolute Value of Power

Methinks 'twould be more valuable to prove the version for a positive real base and real exponent without reference to complex numbers and using "absolute value", and to prove the more general form (complex base; real exponent) as well. --Dfeuer (talk) 02:12, 11 April 2013 (UTC)

Play with it as you'd like, I'm all proofed out right now. --GFauxPas (talk) 02:14, 11 April 2013 (UTC)

How about this (+ links)? --Linus44 (talk) 11:33, 13 April 2013 (UTC)

Sounds like a good idea. Name theorem 2 something like Modulus of Power? The definition of argument does not seem to pin down $\operatorname{arg}$ very well. --Dfeuer (talk) 17:32, 13 April 2013 (UTC)

That should not be a reason not to use the term "argument" - it just means that nobody's got round to attempting to define it rigorously yet. --prime mover (talk) 18:23, 13 April 2013 (UTC)

Since Linus44 appears to know much more about complex analysis than I do, perhaps he can do so. But it's also possible that $\operatorname{arg}$ is inherently a bit tricky to pin down (perhaps having a codomain consisting of equivalence classes and used only in formal equations? I really don't know) so it may be easier to use $\operatorname{Arg}$ instead where appropriate. --Dfeuer (talk) 18:41, 13 April 2013 (UTC)

He probably does. --prime mover (talk) 19:21, 13 April 2013 (UTC)

Theorem 1

Let $z \in \R_{\geq 0}$, $w \in \R$.

Then $|z^w| = |z|^w$.

Proof

Since $z \in \R_{\geq 0}$, $|z| = z$, so it is sufficient to prove that

$z^w = |z^w|$

This is true if and only if $z^w \geq 0$.

But

$z^w = \exp(w \log z)$

Since $z \geq 0$, $\arg(z) = 0$, so by Definition:Logarithm $\log z \in \R$.

Now by Exponential on Real Numbers is Group Isomorphism shows that $\exp(w \log z) = z^w \geq 0$.

Theorem 2

Let $z,w$ be complex numbers.

Then $|z^w| = |z|^w$ if and only if either $z \in \{0,1\}$ or $\Im(w) = 0$.

Proof

Step 1: $ \Leftarrow $

The statement is clear when $z \in \{0,1\}$.

Therefore suppose that $z \neq 0$ and $\Im(w) = 0$.

We have the definition the general complex power:

$z^w = \exp(w\log z) = \exp(w \log |z| + i w\arg(z))$

so by Modulus and Argument of Complex Exponential,

$|z^w| = \exp(\Re(w) \log |z| - \Im(w) \arg(z))$

Now, again by the definition of the general complex power and the complex logarithm,

$|z|^w = \exp(w\log |z|) = \exp(\Re(w)\log |z| + i \Im(w) \log |z|)$

By Exponential on Real Numbers is Group Isomorphism $z \neq 0 \implies z^w \neq 0$, so we can write

$|z^w|^{-1}|z|^w = \exp(i \Im(w) \log |z| - \Im(w) \arg(z))$

and by Exponential of Zero $|z^w|=|z|^w$ iff

$(1):\qquad i \Im(w) \log |z| - \Im(w) \arg(z) = 0$

Since by hypothesis $\Im(w) = 0$, this relation is satisfied by Ring Product with Zero, so we indeed have $|z^w|=|z|^w$.

Step 2: $\Rightarrow$

Suppose that $|z^w|=|z|^w$.

If $z = 0$, the result is clear.

Suppose therefore that $z \neq 0$.

We have from $(1)$:

$|z^w|=|z|^w$ iff $i \Im(w) \log |z| - \Im(w) \arg(z) = 0$

If $\Im(w) \neq 0$, by Complex Numbers form Integral Domain this implies that

$i \log |z| = \arg(z)$

Since by definition $\arg(z) \in \R$, and $\log |z| \in \R$, we can only have this equality if

$\log |z| = \arg(z) = 0$.

Since $\log |z| = 0$, we must have $|z| = 1$.

Since $\arg(z) = 0$, we must have $z \in \R_{\geq 0}$.

Therefore $z = 1$.

Thus either $z \in \{0,1\}$ or $\Im(w) = 0$ as required.

Why is this proof in the discussion page and not on the main theorem? --GFauxPas (talk) 08:24, 9 December 2016 (EST)