Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] complex argument function(s)

view this post on Zulip Email Gateway (Jun 25 2021 at 20:28):

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

view this post on Zulip Email Gateway (Jul 01 2021 at 01:10):

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

view this post on Zulip Email Gateway (Jul 01 2021 at 08:37):

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

view this post on Zulip Email Gateway (Jul 01 2021 at 09:54):

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

view this post on Zulip Email Gateway (Jul 01 2021 at 14:06):

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 mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Jul 01 2021 at 14:07):

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

view this post on Zulip Email Gateway (Jul 01 2021 at 14:27):

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 \nat

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

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

view this post on Zulip Email Gateway (Jul 01 2021 at 14:34):

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 mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Jul 03 2021 at 11:05):

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 mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Jul 03 2021 at 20:22):

From: Manuel Eberl <eberlm@in.tum.de>
I'm happy to have whatever you deem useful moved to the library.

Manuel

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

Last updated: Jul 15 2022 at 23:21 UTC