3.1. Polar form
section Polar_form
A nonzero complex number, like a vector in \mathbb{R}^2, can be written in polar form.
Given any nonzero complex number x + iy, we may write
x + iy = r(\cos\theta + i\sin\theta)
where r > 0 and \theta are real numbers.
The number r is the modulus of x+iy,
representing the length of the corresponding vector, and
\theta is the angle from the positive real axis to that vector.
Proposition 1.4.1. Let
-
z_1 = r_1(\cos\theta_1 + i\sin\theta_1), -
z_2 = r_2(\cos\theta_2 + i\sin\theta_2)
be two complex numbers in polar form. Then
z_1 z_2 = r_1 r_2 \big[\cos(\theta_1 + \theta_2) + i\sin(\theta_1 + \theta_2)\big].
We prove by calculation: expand using i^2=-1, and
apply the angle-addition identities.
theorem polar_mul (r₁ r₂ θ₁ θ₂ : ℝ) :
(r₁ * ((Real.cos θ₁) + (Real.sin θ₁)*I)) *
(r₂ * ((Real.cos θ₂) + (Real.sin θ₂)*I)) =
(r₁*r₂)*((Real.cos (θ₁+θ₂)) + (Real.sin (θ₁+θ₂))*I) :=
calc (r₁ * ((Real.cos θ₁) + (Real.sin θ₁)*I)) *
(r₂ * ((Real.cos θ₂) + (Real.sin θ₂)*I))
/- Step 1 – pull the moduli r₁, r₂ to the front
and distribute the product -/
_ = r₁ * r₂*
((I ^ 2) * Real.sin θ₁ *Real.sin θ₂ +
Real.cos θ₁ * Real.cos θ₂ +
I* Real.cos θ₁ * Real.sin θ₂ +
I * Real.sin θ₁ * Real.cos θ₂) := r₁:ℝr₂:ℝθ₁:ℝθ₂:ℝ⊢ ↑r₁ * (↑(Real.cos θ₁) + ↑(Real.sin θ₁) * I) * (↑r₂ * (↑(Real.cos θ₂) + ↑(Real.sin θ₂) * I)) =
↑r₁ * ↑r₂ *
(I ^ 2 * ↑(Real.sin θ₁) * ↑(Real.sin θ₂) + ↑(Real.cos θ₁) * ↑(Real.cos θ₂) + I * ↑(Real.cos θ₁) * ↑(Real.sin θ₂) +
I * ↑(Real.sin θ₁) * ↑(Real.cos θ₂)) All goals completed! 🐙
-- Step 2 – using I² = −1
_ = r₁ * r₂*
((-1) * Real.sin θ₁ *Real.sin θ₂ +
Real.cos θ₁ * Real.cos θ₂ +
I* Real.cos θ₁ * Real.sin θ₂ +
I * Real.sin θ₁ * Real.cos θ₂) := r₁:ℝr₂:ℝθ₁:ℝθ₂:ℝ⊢ ↑r₁ * ↑r₂ *
(I ^ 2 * ↑(Real.sin θ₁) * ↑(Real.sin θ₂) + ↑(Real.cos θ₁) * ↑(Real.cos θ₂) + I * ↑(Real.cos θ₁) * ↑(Real.sin θ₂) +
I * ↑(Real.sin θ₁) * ↑(Real.cos θ₂)) =
↑r₁ * ↑r₂ *
(-1 * ↑(Real.sin θ₁) * ↑(Real.sin θ₂) + ↑(Real.cos θ₁) * ↑(Real.cos θ₂) + I * ↑(Real.cos θ₁) * ↑(Real.sin θ₂) +
I * ↑(Real.sin θ₁) * ↑(Real.cos θ₂)) All goals completed! 🐙
/- Apply the angle-addition formulas
cos(θ₁ + θ₂) = cos θ₁ cos θ₂ − sin θ₁ sin θ₂
sin(θ₁ + θ₂) = sin θ₁ cos θ₂ + cos θ₁ sin θ₂
recognise the result as cos(θ₁+θ₂)+i sin(θ₁+θ₂) -/
_ = r₁ * r₂ * ((Real.cos (θ₁ + θ₂))
+ I * (Real.sin (θ₁ + θ₂))) := r₁:ℝr₂:ℝθ₁:ℝθ₂:ℝ⊢ ↑r₁ * ↑r₂ *
(-1 * ↑(Real.sin θ₁) * ↑(Real.sin θ₂) + ↑(Real.cos θ₁) * ↑(Real.cos θ₂) + I * ↑(Real.cos θ₁) * ↑(Real.sin θ₂) +
I * ↑(Real.sin θ₁) * ↑(Real.cos θ₂)) =
↑r₁ * ↑r₂ * (↑(Real.cos (θ₁ + θ₂)) + I * ↑(Real.sin (θ₁ + θ₂)))
r₁:ℝr₂:ℝθ₁:ℝθ₂:ℝ⊢ -1 * ↑(Real.sin θ₁) * ↑(Real.sin θ₂) + ↑(Real.cos θ₁) * ↑(Real.cos θ₂) + I * ↑(Real.cos θ₁) * ↑(Real.sin θ₂) +
I * ↑(Real.sin θ₁) * ↑(Real.cos θ₂) =
↑(Real.cos (θ₁ + θ₂)) + I * ↑(Real.sin (θ₁ + θ₂))
r₁:ℝr₂:ℝθ₁:ℝθ₂:ℝ⊢ (-1 * ↑(Real.sin θ₁) * ↑(Real.sin θ₂) + ↑(Real.cos θ₁) * ↑(Real.cos θ₂) + I * ↑(Real.cos θ₁) * ↑(Real.sin θ₂) +
I * ↑(Real.sin θ₁) * ↑(Real.cos θ₂)).re =
(↑(Real.cos (θ₁ + θ₂)) + I * ↑(Real.sin (θ₁ + θ₂))).rer₁:ℝr₂:ℝθ₁:ℝθ₂:ℝ⊢ (-1 * ↑(Real.sin θ₁) * ↑(Real.sin θ₂) + ↑(Real.cos θ₁) * ↑(Real.cos θ₂) + I * ↑(Real.cos θ₁) * ↑(Real.sin θ₂) +
I * ↑(Real.sin θ₁) * ↑(Real.cos θ₂)).im =
(↑(Real.cos (θ₁ + θ₂)) + I * ↑(Real.sin (θ₁ + θ₂))).im r₁:ℝr₂:ℝθ₁:ℝθ₂:ℝ⊢ (-1 * ↑(Real.sin θ₁) * ↑(Real.sin θ₂) + ↑(Real.cos θ₁) * ↑(Real.cos θ₂) + I * ↑(Real.cos θ₁) * ↑(Real.sin θ₂) +
I * ↑(Real.sin θ₁) * ↑(Real.cos θ₂)).re =
(↑(Real.cos (θ₁ + θ₂)) + I * ↑(Real.sin (θ₁ + θ₂))).rer₁:ℝr₂:ℝθ₁:ℝθ₂:ℝ⊢ (-1 * ↑(Real.sin θ₁) * ↑(Real.sin θ₂) + ↑(Real.cos θ₁) * ↑(Real.cos θ₂) + I * ↑(Real.cos θ₁) * ↑(Real.sin θ₂) +
I * ↑(Real.sin θ₁) * ↑(Real.cos θ₂)).im =
(↑(Real.cos (θ₁ + θ₂)) + I * ↑(Real.sin (θ₁ + θ₂))).im
r₁:ℝr₂:ℝθ₁:ℝθ₂:ℝ⊢ (cos ↑θ₁).re * (sin ↑θ₂).re + (sin ↑θ₁).re * (cos ↑θ₂).re = (sin ↑θ₁).re * (cos ↑θ₂).re + (cos ↑θ₁).re * (sin ↑θ₂).re r₁:ℝr₂:ℝθ₁:ℝθ₂:ℝ⊢ -((sin ↑θ₁).re * (sin ↑θ₂).re) + (cos ↑θ₁).re * (cos ↑θ₂).re = (cos ↑θ₁).re * (cos ↑θ₂).re - (sin ↑θ₁).re * (sin ↑θ₂).rer₁:ℝr₂:ℝθ₁:ℝθ₂:ℝ⊢ (cos ↑θ₁).re * (sin ↑θ₂).re + (sin ↑θ₁).re * (cos ↑θ₂).re = (sin ↑θ₁).re * (cos ↑θ₂).re + (cos ↑θ₁).re * (sin ↑θ₂).re
All goals completed! 🐙
-- Step 3 – refold r₁ * r₂ as (r₁ * r₂).
_ = (r₁*r₂) *
((Real.cos (θ₁+θ₂)) + (Real.sin (θ₁+θ₂))*I) :=
r₁:ℝr₂:ℝθ₁:ℝθ₂:ℝ⊢ ↑r₁ * ↑r₂ * (↑(Real.cos (θ₁ + θ₂)) + I * ↑(Real.sin (θ₁ + θ₂))) =
↑r₁ * ↑r₂ * (↑(Real.cos (θ₁ + θ₂)) + ↑(Real.sin (θ₁ + θ₂)) * I) All goals completed! 🐙
A special case of multiplication in polar form when the two radii are both equal to 1.
(\cos θ_1+ i \sin θ_1)*(\cos θ_2+ i \sin θ_2) = \cos (θ_1+θ_2)+ i \sin (θ_1+θ_2)
theorem polar_mul' (θ₁ θ₂ : ℝ) :
((Real.cos θ₁) + (Real.sin θ₁)*I) *
((Real.cos θ₂) + (Real.sin θ₂)*I) =
(Real.cos (θ₁+θ₂)) + (Real.sin (θ₁+θ₂)*I) :=
θ₁:ℝθ₂:ℝ⊢ (↑(Real.cos θ₁) + ↑(Real.sin θ₁) * I) * (↑(Real.cos θ₂) + ↑(Real.sin θ₂) * I) =
↑(Real.cos (θ₁ + θ₂)) + ↑(Real.sin (θ₁ + θ₂)) * I All goals completed! 🐙
Definition 1.4.2. The argument of a nonzero complex number z is the angle from the positive
real axis to the line segment joining 0 to z.
We denote it by \arg(z).
The argument is also called the phase or angle of z.
Definition 1.4.3. (Principal argument)
If we choose the interval (-\pi, \pi] as the range, then for any nonzero complex number
z the principal argument \theta_0 is the unique angle in (-\pi, \pi] satisfying
-
\cos\theta_0 = \frac{\operatorname{Re}(z)}{|z|}, and -
\sin\theta_0 = \frac{\operatorname{Im}(z)}{|z|}.
We write \operatorname{Arg}(z) for the principal argument.
end Polar_form