complex_polar_coordinates

proveit.numbers.complex_polar_coordinates(expr, \*, radius_must_be_nonneg=True, nonneg_radius_preferred=True, do_include_unit_length_reduction=True, reductions=None)

Given an expression, expr, of the complex number polar form,

r * exp(i * theta),

or something obviously equivalent to this, where r and theta are Real (and r is preferably RealNonNeg) under the given assumptions, return

(r, theta)

as a tuple pair.

If radius_must_be_nonneg and nonneg_radius_preferred are False, we won’t worry about ensuring that r is non-negative (so the result can be ambiguous). If radius_must_be_nonneg is True, a ValueError will be raised if we can’t convert to a form where r is known to be non-negative.

If expr is not exactly in this complex number polar form and ‘reductions’ is provided as a set, add to the ‘reductions’ set an equation that equates the exact form on the left with the original form on the right. This may be useful to use as ‘reductions’ in instantiations of theorems that employ the complex number polar form so it may perform proper reductions to the desired form. For example, if expr=5 is provided, the added reduction will be

5 * exp(i * 0) = 5.

If do_include_unit_length_reduction is True, we will included reductions so that it will reduce from the unit length form as well. For example, if expr=1 is provided, the added reductions will be

exp(i * 0) = 1 1 * 1 = 1.

This also works in a way that cascades when reducing from the general polar form:

1 * exp(i * 0) = 1 * 1 = 1

Raise ValueError if the expr is not obviously equivalent to a complex number polar form.

Also see unit_length_complex_polar_angle.