# Zulip Chat Archive

## 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],
simp [mul_add],
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],
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 (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.

#### Patrick Massot (Oct 27 2020 at 22:21):

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.)

#### 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