Defining z.arg using modulus

Stream: new members

[Shadman Sakib]

Since we know modz = 1, then either a or b is 0 in finding modz, i.e, in sqrt(a^2 + b^2). Thus, as a complex number z can be either 1 or i. When z is 1, z.arg is 0 and when z is i z.arg is pi/2. How can Lean understand this?

[Shadman Sakib]

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric
import data.real.pi
noncomputable theory

open complex dihedral_group

local notation `|` x `|` := complex.abs x
local notation `π` := real.pi

example (z : ℂ) (hz : |z| = 1) : z.arg = 0 ∨ z.arg = π / 2 :=
begin
  admit,
end

[Eric Wieser]

Why can't z be 0.6+0.8i?

[Eric Wieser]

Which as far as I can tell makes your lemma false

[Eric Wieser]

Even z = -1 is a counterexample

[Shadman Sakib]

Is there a way to understand z.arg given modulus z?

[Shadman Sakib]

Mathematically, since z can consist of negative or positive real/imaginary parts z.arg cannot be defined in one equation, right?

[Eric Wieser]

I don't understand your question. Knowing complex.arg z tells you nothing about complex.abs z, and vice versa so long as z ≠ 0

[Eric Wieser]

The only conclusion you can make that is remotely like what you're asking for us that complex.abs z = 0 → complex.arg z = 0, but that's not very interesting

[Shadman Sakib]

OK, the reason I am asking is because I do not know how to "assign" a value to z.arg in this proof with the information that I am given. I know z is on the unit circle from the hypothesis, but it does not tell me anything about z.arg without a particular value z. I will provide an #mwe but please do not solve the proof.

[Shadman Sakib]

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric
import data.real.pi
noncomputable theory

open complex dihedral_group

local notation `|` x `|` := complex.abs x
local notation `π` := real.pi

example (z : ℂ) (hz : |z| = 1) : exp (↑(z.arg) * I) = z :=
begin
  admit,
end

[Shadman Sakib]

Is there a way to simplify the goal state, specifically simplifying z.arg?

[Vasu]

Hi everyone, I am very new to Lean, is there an equivalent of Coq's "Example" in Lean?

[Horatiu Cheval]

Could you please ask the question in a new thread (by specifying another topic when posting the message)? You posted it in a thread that's about something else

[Kevin Buzzard]

How can you "simplify" z.arg? It just means "apply the arg function to the variable zwhich has no definition"

[Kevin Buzzard]

A better question would be "what is the maths proof you are trying to formalise"? The answer "this statement is obvious and I just want it to go away" is not sufficient.

[Eric Wieser]

The statement is false, consider z = 1 (edit: it is too early)

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

In the proof I'm thinking of you would not be simplifying this expression but complifying it a little first

[Kevin Buzzard]

PS why do you post example after example of questions in complex analysis with all those extraneous imports and opens and notations? As an exercise, why not try and take the code you posted last and actually make the example minimal, with no irrelevant lines of code? This is what #mwe means. This will make your questions easier to understand. Delete some random lines of code from your post and if things still compile then your question has got better.

[Eric Wieser]

Removing imports makes your code not only easier to follow, but faster to load in the web editor (I believe)

[Eric Wieser]

The statement is (unsurprisingly) true after all, I was able to mostly prove it using docs#complex.exp_log. You should write down the maths proof, and get lean to go through the intermediate step

[Kevin Buzzard]

I think that you shouldn't be using random extensions of log to the complex plane here. You should use the theorem that if |z|=r and arg(z)=theta then z=re^{i theta}. This is the mathematically reasonable way to prove the result

[Eric Wieser]

I agree, but couldn't find that result

[Eric Wieser]

These don't seem to succeed for me (although my patience for library_search is low):

import analysis.special_functions.trigonometric

example (z : ℂ) : z = |z| * exp (↑(z.arg) * I) :=
by library_search -- fail

example (z : ℂ) : z = |z| • exp (z.arg • I) :=
by library_search -- fail

example (z : ℂ) : z = |z| * exp (↑(z.arg) * I) :=
by simp -- fail, makes no progress

example (z : ℂ) : z = |z| • exp (z.arg • I) :=
by simp -- fail, makes progress only to the above example

[Kevin Buzzard]

:-/

[Kevin Buzzard]

Well then the fault is with our library

[Ruben Van de Velde]

If someone wants to add it:

example (z : ℂ) : z = z.abs • exp (z.arg • I) :=
begin
  obtain rfl|H := eq_or_ne z 0,
  { simp },
  ext,
  { simp [exp_re, complex.cos_arg H, mul_div_cancel' _ (abs_ne_zero.mpr H)] },
  { simp [exp_im, complex.sin_arg, mul_div_cancel' _ (abs_ne_zero.mpr H)] }
end

[Eric Wieser]

Based on the fact that simp removes smul, it should probably be stated with *

[Eric Wieser]

Either that or we should tell simp to go the other way, but I suspect that breaks a lot of things