From: Lawrence Paulson <lp15@cam.ac.uk>

I’ve just noticed that we define both arg and Arg, the latter in Complex_Transcendental.

The definitions are different but arg z = Arg z holds unconditionally. It looks like a historical accident, maybe arg was introduced in the 1990s and forgotten about.

Interestingly enough, arg is used far more despite there being almost nothing proved about it. Some lemmas are proved in Complex_Geometry/More_Complex.thy, and many occurrences of “arg” are simply variables.

This is a mess. Any suggestions? Maybe Arg could (temporarily) be made an abbreviation for arg. Arg is the usual of the function (principal value of the argument).

Larry

isabelle-dev mailing list

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>

Usually in the literature it's -\pi < Arg z \leq \pi

while arg z = Arg z + 2 \pi N, where N \in \nat

(though sometimes several authors may use these interchangeably or it

could vary)

A suggestion would be to follow the above literature convention in the

Library definitions too

(if practical enough)

Best,

Angeliki

isabelle-dev mailing list

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Manuel Eberl <eberlm@in.tum.de>

I don't understand what the second one means. Is this a multi-valued

function or what does the "N" mean here?

I agree with Larry that one of the two "arg" functions has to go. As for

which one, I have no preference. Making one of them into an abbreviation

sounds reasonable, although I am not sure if it really is less work than

just replacing it in one go immediately.

Note that we also have "is_Arg" and "Arg2pi", so perhaps "Arg" would be

more consistent than "arg".

Manuel

smime.p7s

From: Lawrence Paulson <lp15@cam.ac.uk>

Oh yes, the old convention: when you have a multi-valued function, the “principal value” is capitalised. In the case of Isabelle/HOL, that means we need to choose the name Arg, not arg. To smooth the changeover, surely it’s best to leave the first definition (but now capitalised) where it is and replace the second definition by the same statement but proved as a theorem. At least a renaming is relatively easy to accomplish even if it triggers hundreds of errors.

Remark number one: for some reason, the HOL Light library defines Arg to range from 0 to 2pi. Although some authors make that choice, you then have to define Ln similarly so that you have Arg z = Im (Ln z). It’s truly bizarre that this identity fails in HOL Light.

Remark number two: I dug into this because of constructions involving Arg in that Apostol volume that turned out to have nothing to do with anything.

Larry

isabelle-dev mailing list

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>

yes, arg z is multi-valued,

and N measures how many rotations around the axis you do, while Arg z is

just the principal value.

And I should have written N \in \int (not N \in \nat) in my previous

message!

Best,

Angeliki

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Manuel Eberl <eberlm@in.tum.de>

Well, that does not make much sense in Isabelle/HOL. HOL doesn't have

multivalued functions.

We can only emulate such things with e.g. relations, which is what

is_Arg does.

Manuel

smime.p7s

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>

Remark number one: for some reason, the HOL Light library defines

Arg

to range from 0 to 2pi. Although some authors make that choice, you

then have to define Ln similarly so that you have Arg z = Im (Ln z).

It’s truly bizarre that this identity fails in HOL Light.

On 2021-07-01 10:53, Lawrence Paulson wrote:

Oh yes, the old convention: when you have a multi-valued function, the

“principal value” is capitalised. In the case of Isabelle/HOL, that

means we need to choose the name Arg, not arg. To smooth the

changeover, surely it’s best to leave the first definition (but now

capitalised) where it is and replace the second definition by the same

statement but proved as a theorem. At least a renaming is relatively

easy to accomplish even if it triggers hundreds of errors.

I agree with Larry that this sounds like the optimal solution.

Remark number one: for some reason, the HOL Light library defines Arg

to range from 0 to 2pi. Although some authors make that choice, you

then have to define Ln similarly so that you have Arg z = Im (Ln z).

It’s truly bizarre that this identity fails in HOL Light.

Which of the range conventions would you prefer to keep? I think any one

is fine as long as things are

all consistent

Best,

Angeliki

On 1 Jul 2021, at 09:37, Manuel Eberl <eberlm@in.tum.de> wrote:

On 01/07/2021 03:09, Dr A. Koutsoukou-Argyraki wrote:

Usually in the literature it's -\pi < Arg z \leq \pi

while arg z = Arg z + 2 \pi N, where N \in \natI don't understand what the second one means. Is this a multi-valued

function or what does the "N" mean here?I agree with Larry that one of the two "arg" functions has to go. As

for

which one, I have no preference. Making one of them into an

abbreviation

sounds reasonable, although I am not sure if it really is less work

than

just replacing it in one go immediately.Note that we also have "is_Arg" and "Arg2pi", so perhaps "Arg" would

be

more consistent than "arg".Manuel

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>

I was only commenting on the most common naming convention within the

maths literature regarding arg VS Arg.

Best,

Angeliki

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Lawrence Paulson <lp15@cam.ac.uk>

Yesterday I renamed arg -> Arg along with most of the arg_ theorems (though we still have arg_unique and Arg_unique).

I noticed some useful-looking basic lemmas about Arg in Stirling_Formula/Gamma_Asymptotics.thy (added to the AFP by Manuel in 2016) that we might bring into the libraries. Any comments?

Larry

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Manuel Eberl <eberlm@in.tum.de>

I'm happy to have whatever you deem useful moved to the library.

Manuel

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Feb 24 2024 at 04:17 UTC