[isabelle-dev] complex argument function(s)

[Dr A. Koutsoukou-Argyraki]

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



On 2021-06-25 21:28, Lawrence Paulson wrote:
> 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 at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev