Exponential form of a complex number

Stream: maths

[Gihan Marasingha]

Is there a canonical way to express a complex number in exponential form. This is what I've done, but it seems long-winded.

import data.complex.exponential
import analysis.special_functions.pow

noncomputable theory

open complex

-- Aim to show `u = u₂`
def θ := -real.pi/4
def u := 10*(cos θ + (sin θ)*I)
def u₂ : ℂ := 5 * (real.sqrt 2)*(1 + (-1)*I)

-- We need a few lemmas that aren't in mathlib
namespace complex

lemma cos_pi_div_four : complex.cos ((real.pi / 4) : ℝ) = real.sqrt 2 / 2 :=
begin
  rw ←(re_add_im (complex.cos ((real.pi / 4) : ℝ))),
  rw [complex.cos_of_real_re, complex.cos_of_real_im, real.cos_pi_div_four],
  simp,
end

lemma sin_pi_div_four : complex.sin ((real.pi / 4) : ℝ)  = real.sqrt 2 / 2 :=
begin
  rw ←(re_add_im (complex.sin ((real.pi / 4) : ℝ))),
  rw [complex.sin_of_real_re, complex.sin_of_real_im, real.sin_pi_div_four],
  simp,
end

end complex

example : u = u₂ :=
begin
  unfold u u₂ θ,
  rw [complex.of_real_div,complex.of_real_neg,neg_div,cos_neg,sin_neg],
  rw [←complex.of_real_div, complex.cos_pi_div_four, complex.sin_pi_div_four],
  ring,
end

[Mario Carneiro]

well an obvious improvement would be to use exp (I * theta)

[Kenny Lau]

isn't that just one lemma away™?

[Gihan Marasingha]

Once I've rewritten with exp, how can I show u = u₂?

Edit: above, I need to use a result complex.cos_pi_div_four. Is there an equivalent result exp_I_pi_div_four? Or some other clever way to work with exp?

[Mario Carneiro]

lemma exp_I_pi_div_four : exp ((real.pi / 4 : ℝ) * I) = real.sqrt 2 / 2 * (1 + I) :=
begin
  rw [exp_mul_I, ← of_real_cos, ← of_real_sin, real.cos_pi_div_four, real.sin_pi_div_four],
  simp [mul_add],
end

[Mario Carneiro]

-- Aim to show `u = u₂`
def θ := -real.pi/4
def u := 10 * exp (θ * I)
def u₂ : ℂ := 5 * (real.sqrt 2)*(1 + (-1)*I)

-- We need a few lemmas that aren't in mathlib
namespace complex

lemma exp_I_pi_div_four : exp ((real.pi / 4 : ℝ) * I) = real.sqrt 2 / 2 * (1 + I) :=
begin
  rw [exp_mul_I, ← of_real_cos, ← of_real_sin, real.cos_pi_div_four, real.sin_pi_div_four],
  simp [mul_add],
end

end complex

example : u = u₂ :=
begin
  rw ← conj_inj,
  unfold u u₂,
  simp [← exp_conj],
  rw [neg_mul_eq_neg_mul, ← of_real_neg, θ, neg_div, neg_neg, complex.exp_I_pi_div_four],
  ring,
end

[Gihan Marasingha]

Thanks very much! Much nicer.

[Heather Macbeth]

Here's an issue I encountered while experimenting with this. I'd have thought simp would deal with the following (because of the simp-lemma docs#complex.of_real_im), but it doesn't:

import analysis.special_functions.pow
import data.complex.basic

example : (((real.sqrt 2) / 2) : ℂ).im = 0 :=
begin
  exact complex.of_real_im _,
end

[Heather Macbeth]

Error:

invalid type ascription, term has type
  ↑?m_1.im = 0
but is expected to have type
  (↑(real.sqrt 2) / 2).im = 0

[Patrick Massot]

exact_mod_cast maybe?

[Mario Carneiro]

yeah, we have some non-confluent simp lemmas here

[Mario Carneiro]

oh, you aren't using simp

[Heather Macbeth]

(simp fails too, but I was trying to reverse-engineer what I wanted simp to do)

[Mario Carneiro]

this is just because lean elaborates from outside in, the arrows go on the innermost term

[Mario Carneiro]

you have to write (\u ((real.sqrt 2) / 2) : ℂ).im = 0 if you want the arrow in the right place

[Patrick Massot]

Funnily, my suggestion works but only after replacing the underscore by (real.sqrt 2/2).

[Heather Macbeth]

The problem was that I didn't write ((real.sqrt 2) / 2) myself; it turned up in the proof, created by previous lemmas. I'll try to find which one; maybe that one needs to be stated with a different cast setup.

[Patrick Massot]

The funny part is that exact_mod_cast succeeds but creates a new goal asking for the real number to be used.

[Rob Lewis]

Patrick Massot said:

The funny part is that exact_mod_cast succeeds but creates a new goal asking for the real number to be used.

This looks like a bug in exact_mod_cast, feel free to open an issue.

[Rob Lewis]

This is exactly the use case for that tactic so it should work.

[Rob Lewis]

As should apply_mod_cast

[Patrick Massot]

Side note: Heather, you don't need parentheses around real.sqrt 2. Function application has really high precedence.

[Rob Lewis]

In fact, norm_cast proves this on its own. The bad behavior is probably a result of the (\u r).im = 0 lemmas that don't fit the algorithm particularly well.

[Patrick Massot]

Too late, I opened #4805

[Heather Macbeth]

OK, so here's a proof of @Gihan Marasingha 's fact that is nearly without trig-specific knowledge:

import data.complex.exponential
import analysis.special_functions.pow

noncomputable theory
open real

-- Aim to show `u = u₂`
def θ := - (real.pi / 4)
def u := (10:ℂ) * (cos θ + (sin θ) * complex.I)
def u₂ : ℂ := 5 * (real.sqrt 2) * (1 + (-1)*complex.I)

example : u = u₂ :=
begin
  simp [u, u₂, θ, cos_pi_div_four, sin_pi_div_four],
  ext,
  { simp,
    exact_mod_cast _,
    ring },
  { simp,
    exact_mod_cast _,
    ring }
end

If we make cos_pi_div_four and sin_pi_div_four simp-lemmas, it can be entirely so. (It seems like it's just an omission that they're not simp-lemmas; cos_pi_div_two and tan_pi_div_four are.)

[Heather Macbeth]

(note that this is not mathlib-style, though, because it has nonterminal simps)

[Patrick Massot]

What are those exact_mod_cast _? Do you mean norm_cast?

[Mario Carneiro]

you could write that latter part ext; { simp, exact_mod_cast _, ring },

[Patrick Massot]

Those non-terminal simps are ok because they are followed only by end-game tactics.

[Heather Macbeth]

Mario Carneiro said:

you could write that latter part ext; { simp, exact_mod_cast _, ring },

I know, but @Gihan Marasingha's students may not!

[Mario Carneiro]

(my proof also has nonterminal simps btw, but the simp only line is a little distracting)

[Heather Macbeth]

Patrick Massot said:

Those non-terminal simps are ok because they are followed only by end-game tactics.

This I didn't know!

[Rob Lewis]

example : u = u₂ :=
begin
  ext; { simp [u, u₂, θ, cos_pi_div_four, sin_pi_div_four], norm_cast, ring }
end

is almost legit. Following simp with norm_cast is borderline.

[Patrick Massot]

Oh, I didn't see the first simp. Rob's version is better indeed.

[Rob Lewis]

norm_cast sort of cares about the details of the goal. It's plausible that simp lemmas could change the positions of casts in a way that would break norm_cast, but reasonably unlikely.

[Patrick Massot]

Fair enough.

[Mario Carneiro]

particularly in this case because of the non-confluence - it might eliminate them entirely and then norm_cast would fail

[Heather Macbeth]

Heather Macbeth said:

If we make cos_pi_div_four and sin_pi_div_four simp-lemmas, it can be entirely so. (It seems like it's just an omission that they're not simp-lemmas; cos_pi_div_two and tan_pi_div_four are.)

Shall I add cos_pi_div_four etc to the simp-set?

[Heather Macbeth]

Rob Lewis said:

norm_cast sort of cares about the details of the goal. It's plausible that simp lemmas could change the positions of casts in a way that would break norm_cast, but reasonably unlikely.

Is there a more idiomatic way to do this kind of thing, perhaps a simp variant that omits casting lemmas from the simp-set?

[Rob Lewis]

Mm, not really. If the simp only is too big I wouldn't worry too much about this particular nonterminal simp.

[Heather Macbeth]

Heather Macbeth said:

If we make cos_pi_div_four and sin_pi_div_four simp-lemmas, it can be entirely so. (It seems like it's just an omission that they're not simp-lemmas; cos_pi_div_two and tan_pi_div_four are.)

#4806

[Heather Macbeth]

@Gihan Marasingha #4806 is now merged and your lemma can be entirely automated:

import analysis.special_functions.trigonometric

noncomputable theory
open real

-- Aim to show `u = u₂`
def θ := - (pi / 4)
def u := (10:ℂ) * (cos θ + (sin θ) * complex.I)
def u₂ : ℂ := 5 * (sqrt 2) * (1 + (-1) * complex.I)

example : u = u₂ :=
by ext; { simp [u, u₂, θ], norm_cast, ring }

[Gihan Marasingha]

@Heather Macbeth amazing! Thanks so much.