3.2. DeMoivre formula
section DeMoivre_formula
Theorem 1.4.4. (DeMoivre's formula)
For any n \in \mathbb{Z} and \theta \in \mathbb{R},
(\cos\theta + i\sin\theta)^n = \cos(n\theta) + i\sin(n\theta)
We first prove DeMoivre formula for nonnegative integer n.
The proof proceeds by induction.
/-- Prove by using the tactic `induction` -/
theorem DeMoivre (θ : ℝ) (n : ℕ) :
(Real.cos θ+(Real.sin θ)*I) ^ n =
Real.cos (n*θ) + Real.sin (n*θ) * I := θ:ℝn:ℕ⊢ (↑(Real.cos θ) + ↑(Real.sin θ) * I) ^ n = ↑(Real.cos (↑n * θ)) + ↑(Real.sin (↑n * θ)) * I
-- 1. Start Induction on n
induction n with
θ:ℝ⊢ (↑(Real.cos θ) + ↑(Real.sin θ) * I) ^ 0 = ↑(Real.cos (↑0 * θ)) + ↑(Real.sin (↑0 * θ)) * I
/- Base case: n = 0
LHS = (...)^0 = 1
RHS = cos 0 + sin 0 * I = 1 + 0 = 1 -/
All goals completed! 🐙
θ:ℝn:ℕih:(↑(Real.cos θ) + ↑(Real.sin θ) * I) ^ n = ↑(Real.cos (↑n * θ)) + ↑(Real.sin (↑n * θ)) * I⊢ (↑(Real.cos θ) + ↑(Real.sin θ) * I) ^ (n + 1) = ↑(Real.cos (↑(n + 1) * θ)) + ↑(Real.sin (↑(n + 1) * θ)) * I
/-Inductive step: Assume true for n, prove for n + 1
Rewrite z^(n+1) as z^n * z, and
apply the induction hypothesis -/
θ:ℝn:ℕih:(↑(Real.cos θ) + ↑(Real.sin θ) * I) ^ n = ↑(Real.cos (↑n * θ)) + ↑(Real.sin (↑n * θ)) * I⊢ (↑(Real.cos (↑n * θ)) + ↑(Real.sin (↑n * θ)) * I) * (↑(Real.cos θ) + ↑(Real.sin θ) * I) =
↑(Real.cos (↑(n + 1) * θ)) + ↑(Real.sin (↑(n + 1) * θ)) * I
-- simplify by multiplying in polar form
θ:ℝn:ℕih:(↑(Real.cos θ) + ↑(Real.sin θ) * I) ^ n = ↑(Real.cos (↑n * θ)) + ↑(Real.sin (↑n * θ)) * I⊢ ↑(Real.cos (↑n * θ + θ)) + ↑(Real.sin (↑n * θ + θ)) * I = ↑(Real.cos (↑(n + 1) * θ)) + ↑(Real.sin (↑(n + 1) * θ)) * I
All goals completed! 🐙
Next, prove the DeMoivre formula for negative exponent.
We need two helper lemmas. We first show that
\cos x + i \sin x ≠ 0 by reduction to \cos ^2 x + \sin ^2x =1.
/-- Helper lemma 1
cos x + (sin x)*I ≠ 0
-/
lemma cos_add_sin_mul_I_ne_zero (x : ℝ) :
(Real.cos (x) + Real.sin (x) * I : ℂ) ≠ 0 := x:ℝ⊢ ↑(Real.cos x) + ↑(Real.sin x) * I ≠ 0
x:ℝ⊢ (cos ↑x).re = 0 → ¬(sin ↑x).re = 0;
x:ℝ⊢ Real.cos x = 0 → ¬Real.sin x = 0
intro h1 x:ℝh1:Real.cos x = 0h2:Real.sin x = 0⊢ False
All goals completed! 🐙 ;
Using the first helper lemma, compute the inverse of
\cos x + i \sin x.
/-- Helper lemma 2
The inverse of (cos (x) + sin (x) *I)
equals cos (-x) + sin (-x) *I
-/
lemma DeMoivre_helper (x : ℝ) :
1 / (Real.cos (x) + Real.sin (x) * I)
= Real.cos (-x) + Real.sin (-x) * I := x:ℝ⊢ 1 / (↑(Real.cos x) + ↑(Real.sin x) * I) = ↑(Real.cos (-x)) + ↑(Real.sin (-x)) * I
x:ℝ⊢ ↑(Real.cos x) + ↑(Real.sin x) * I ≠ 0x:ℝ⊢ 1 = (↑(Real.cos (-x)) + ↑(Real.sin (-x)) * I) * (↑(Real.cos x) + ↑(Real.sin x) * I)
x:ℝ⊢ ↑(Real.cos x) + ↑(Real.sin x) * I ≠ 0 All goals completed! 🐙
x:ℝ⊢ 1 = (↑(Real.cos (-x)) + ↑(Real.sin (-x)) * I) * (↑(Real.cos x) + ↑(Real.sin x) * I) x:ℝ⊢ 1 = Real.cos x * Real.cos x + Real.sin x * Real.sin x ∧ 0 = Real.cos x * Real.sin x + -(Real.sin x * Real.cos x)
exact ⟨x:ℝ⊢ 1 = Real.cos x * Real.cos x + Real.sin x * Real.sin x All goals completed! 🐙,
x:ℝ⊢ 0 = Real.cos x * Real.sin x + -(Real.sin x * Real.cos x) All goals completed! 🐙⟩
Prove that DeMoivre formula holds for negative integer n.
/-- DeMoivre formula for negative integer
-/
theorem DeMoivre_neg_exp (x : ℝ) (n : ℕ) :
1/(Real.cos (x) + Real.sin (x) *I)^n
= Real.cos (-n*x) + (Real.sin (-n*x))*I := x:ℝn:ℕ⊢ 1 / (↑(Real.cos x) + ↑(Real.sin x) * I) ^ n = ↑(Real.cos (-↑n * x)) + ↑(Real.sin (-↑n * x)) * I
have hD : 1/(Real.cos (x) + Real.sin (x) *I)^n
= Real.cos (n*(-x)) + Real.sin (n*(-x)) * I := x:ℝn:ℕ⊢ 1 / (↑(Real.cos x) + ↑(Real.sin x) * I) ^ n = ↑(Real.cos (-↑n * x)) + ↑(Real.sin (-↑n * x)) * I
x:ℝn:ℕ⊢ (1 / (↑(Real.cos x) + ↑(Real.sin x) * I)) ^ n = ↑(Real.cos (↑n * -x)) + ↑(Real.sin (↑n * -x)) * I
x:ℝn:ℕ⊢ (↑(Real.cos (-x)) + ↑(Real.sin (-x)) * I) ^ n = ↑(Real.cos (↑n * -x)) + ↑(Real.sin (↑n * -x)) * I
All goals completed! 🐙
calc
1/(Real.cos (x) + Real.sin (x) *I)^n
_ = Real.cos (n*(-x)) + Real.sin (n*(-x)) * I := hD
_ = Real.cos (-n*x) + Real.sin (-n*x) * I := x:ℝn:ℕhD:1 / (↑(Real.cos x) + ↑(Real.sin x) * I) ^ n = ↑(Real.cos (↑n * -x)) + ↑(Real.sin (↑n * -x)) * I⊢ ↑(Real.cos (↑n * -x)) + ↑(Real.sin (↑n * -x)) * I = ↑(Real.cos (-↑n * x)) + ↑(Real.sin (-↑n * x)) * I All goals completed! 🐙
Finally, we prove DeMoivre's formula for all integers.
/-- DeMoivre formula for all integers
-/
theorem DeMoivre_formula (θ : ℝ) (n : ℤ) :
(Real.cos θ + (Real.sin θ) * I)^n
= (Real.cos (n*θ) + (Real.sin (n*θ))*I) := θ:ℝn:ℤ⊢ (↑(Real.cos θ) + ↑(Real.sin θ) * I) ^ n = ↑(Real.cos (↑n * θ)) + ↑(Real.sin (↑n * θ)) * I
cases n with
θ:ℝm:ℕ⊢ (↑(Real.cos θ) + ↑(Real.sin θ) * I) ^ Int.ofNat m =
↑(Real.cos (↑(Int.ofNat m) * θ)) + ↑(Real.sin (↑(Int.ofNat m) * θ)) * I
-- Case 1: n is a non-negative integer
-- Lean understands `Int.ofNat m` as natural number `m`,
-- so this exactly matches our established theorem
-- for natural numbers.
All goals completed! 🐙
θ:ℝm:ℕ⊢ (↑(Real.cos θ) + ↑(Real.sin θ) * I) ^ Int.negSucc m =
↑(Real.cos (↑(Int.negSucc m) * θ)) + ↑(Real.sin (↑(Int.negSucc m) * θ)) * I
-- Case 2: n is a strictly negative integer
-- In Lean, The constructor `negSucc m` represents the
-- integer `-(m + 1)`.
-- Step 1: Expand the negative integer definitions.
-- `zpow_neg` converts the negative integer power into
-- an inverse: `z ^ -(m+1)` becomes `(z ^ (m+1))⁻¹`.
-- `Int.cast_neg` pushes the negative sign to
-- the RHS angle: `n * θ` becomes `-(m+1) * θ`.
θ:ℝm:ℕ⊢ ((↑(Real.cos θ) + ↑(Real.sin θ) * I) ^ (↑m + 1))⁻¹ = ↑(Real.cos (-↑(↑m + 1) * θ)) + ↑(Real.sin (-↑(↑m + 1) * θ)) * I
-- Step 2: Convert the inverse notation (x⁻¹) into
-- division notation (1 / x).
-- This ensures our goal's syntax perfectly aligns with
-- `DeMoivre_neg_exp`.
θ:ℝm:ℕ⊢ 1 / (↑(Real.cos θ) + ↑(Real.sin θ) * I) ^ (↑m + 1) = ↑(Real.cos (-↑(↑m + 1) * θ)) + ↑(Real.sin (-↑(↑m + 1) * θ)) * I
-- Step 3: Conclude the proof by applying our
-- negative exponent helper theorem.
All goals completed! 🐙
end DeMoivre_formula