Stream: maths

Topic: Exponential form of a complex number

Gihan Marasingha (Oct 27 2020 at 21:27):

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 (Oct 27 2020 at 21:31):

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

Kenny Lau (Oct 27 2020 at 21:32):

isn't that just one lemma away™?

Gihan Marasingha (Oct 27 2020 at 21:38):

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 (Oct 27 2020 at 21:54):

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],
end


Mario Carneiro (Oct 27 2020 at 21:57):

-- 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],
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 (Oct 27 2020 at 21:59):

Thanks very much! Much nicer.

Heather Macbeth (Oct 27 2020 at 22:04):

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 (Oct 27 2020 at 22:04):

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 (Oct 27 2020 at 22:05):

exact_mod_cast maybe?

Mario Carneiro (Oct 27 2020 at 22:05):

yeah, we have some non-confluent simp lemmas here

Mario Carneiro (Oct 27 2020 at 22:06):

oh, you aren't using simp

Heather Macbeth (Oct 27 2020 at 22:06):

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

Mario Carneiro (Oct 27 2020 at 22:07):

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

Mario Carneiro (Oct 27 2020 at 22:07):

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

Patrick Massot (Oct 27 2020 at 22:08):

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

Heather Macbeth (Oct 27 2020 at 22:09):

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 (Oct 27 2020 at 22:09):

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

Rob Lewis (Oct 27 2020 at 22:10):

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 (Oct 27 2020 at 22:10):

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

Rob Lewis (Oct 27 2020 at 22:11):

As should apply_mod_cast

Patrick Massot (Oct 27 2020 at 22:12):

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

Rob Lewis (Oct 27 2020 at 22:15):

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 (Oct 27 2020 at 22:15):

Too late, I opened #4805

Heather Macbeth (Oct 27 2020 at 22:16):

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 (Oct 27 2020 at 22:16):

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

Patrick Massot (Oct 27 2020 at 22:18):

What are those exact_mod_cast _? Do you mean norm_cast?

Mario Carneiro (Oct 27 2020 at 22:18):

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

Patrick Massot (Oct 27 2020 at 22:19):

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

Heather Macbeth (Oct 27 2020 at 22:19):

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 (Oct 27 2020 at 22:19):

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

Heather Macbeth (Oct 27 2020 at 22:20):

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 (Oct 27 2020 at 22:20):

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 (Oct 27 2020 at 22:20):

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

Rob Lewis (Oct 27 2020 at 22:21):

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.

Fair enough.

Mario Carneiro (Oct 27 2020 at 22:21):

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

Heather Macbeth (Oct 27 2020 at 22:22):

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 (Oct 27 2020 at 22:23):

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 (Oct 27 2020 at 22:27):

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

Heather Macbeth (Oct 27 2020 at 22:34):

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 (Oct 28 2020 at 23:13):

@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 (Oct 28 2020 at 23:17):

@Heather Macbeth amazing! Thanks so much.

Last updated: May 18 2021 at 07:19 UTC