Zulip Chat Archive

Stream: new members

Topic: Defining z.arg using modulus


Shadman Sakib (Jul 28 2021 at 23:06):

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 (Jul 28 2021 at 23:06):

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 (Jul 28 2021 at 23:09):

Why can't z be 0.6+0.8i?

Eric Wieser (Jul 28 2021 at 23:10):

Which as far as I can tell makes your lemma false

Eric Wieser (Jul 28 2021 at 23:11):

Even z = -1 is a counterexample

Shadman Sakib (Jul 28 2021 at 23:14):

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

Shadman Sakib (Jul 28 2021 at 23:16):

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

Eric Wieser (Jul 28 2021 at 23:27):

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 (Jul 28 2021 at 23:29):

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 (Aug 01 2021 at 01:24):

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 (Aug 01 2021 at 01:25):

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 (Aug 01 2021 at 01:28):

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

Vasu (Aug 01 2021 at 05:27):

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

Horatiu Cheval (Aug 01 2021 at 06:39):

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 (Aug 01 2021 at 10:38):

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

Kevin Buzzard (Aug 01 2021 at 10:39):

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 (Aug 01 2021 at 10:39):

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

Kevin Buzzard (Aug 01 2021 at 10:40):

(deleted)

Kevin Buzzard (Aug 01 2021 at 10:41):

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

Kevin Buzzard (Aug 01 2021 at 10:43):

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 (Aug 01 2021 at 10:44):

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

Eric Wieser (Aug 01 2021 at 10:46):

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 (Aug 01 2021 at 10:55):

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 (Aug 01 2021 at 11:00):

I agree, but couldn't find that result

Eric Wieser (Aug 01 2021 at 11:05):

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 (Aug 01 2021 at 11:08):

:-/

Kevin Buzzard (Aug 01 2021 at 11:08):

Well then the fault is with our library

Ruben Van de Velde (Aug 01 2021 at 11:47):

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 (Aug 01 2021 at 11:58):

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

Eric Wieser (Aug 01 2021 at 11:58):

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


Last updated: Dec 20 2023 at 11:08 UTC