Multivalued functions/branch cuts.

Stream: Is there code for X?

[James Davenport]

We (Bath/Coventry) note that the definition for log (for example) in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Complex/Log.html defines log with an imaginary part in (-π,π]. While this works, there is no lemma that we see for log(x*y) outside the principal branch, or other results that require branch cut negotiations. Conversely, there don’t seem to be any definitions for the multivalued functions (i.e. with a “+2kiπ” term) which would be another way to state these results.

Are we missing something?

[Antoine Chambert-Loir]

There are no multivalued functions in type theory. If you want to have the multivalued logarithm, its natural target type is $\mathbf C / 2\pi i \mathbf Z$, and then it's the inverse of the natural map induced by exponential after passing to quotient. On the other hand, other determinations of the logarithm would be definitely useful for some computations, for example the one that has an argument in $[0;2\pi\mathclose[$.

[Kevin Buzzard]

I could envisage having a Complex.log' with argument in $[0,2\pi)$ if an argument were made saying that it really is useful for something and using log was somehow more painful.

[Bhavik Mehta]

Note also docs#Complex.log_exp_exists which might help in your application

[Antoine Chambert-Loir]

Kevin Buzzard said:

I could envisage having a Complex.log' with argument in $[0,2\pi)$ if an argument were made saying that it really is useful for something and using log was somehow more painful.

Standard applications are computations of real integrals from $0$ to $+\infty$ using contour integrals where that determination is useful (the idea is to multiply the function to be integrated by $\log'(z)$ and have a contour that goes from $+\infty-i\varepsilon$ to $\varepsilon-i\varepsilon$, circles clockwise to $\varepsilon+i\varepsilon$ and goes to $+\infty+i\varepsilon$, using the fact that $\log'(x+i\varepsilon)\approx \log(x)$, while $\log'(x-i\varepsilon)\approx \log(x)+2i\pi$.

But in fear of missing yet other determinations, I'd rather have a variant of log that prescribes the angle of along which half line it is not continuous.

[James Davenport]

By a "multi-valued function" a meant a function whose values are in the powerset of C, except these are rather special subsets of C, typically {v+2ki\pi: k\in Z} or some such. One can regard this, as you suggest, as a value in C/2πiZ, but then the problem is tracking correlations.

[Jireh Loreaux]

The problem with a multivalued function multiLog : ℂ → Set ℂ that you describe is that working with the resulting sets you get is tedious, and it's hard to "get out of the Set monad", in the sense, that if you want to apply a function ℂ → ℂ afterwards, then you actually have to apply it to images. In other words: (Complex.exp '' · ) ∘ multiLog : ℂ → Set ℂ, and this is the map x ↦ {x} (except for x = 0), which is "single-valued" in some sense, but isn't a function ℂ → ℂ. You can extract such a function, but it's painful.

[Jireh Loreaux]

I guess a key question is: what do you want to do with the branch cuts?

[James Davenport]

Various things:
1)     Know where they are (which humans can do) and what they do to functions, e.g. log(z) drops by 2i π when crossing arg(z)= π.
2)     Work out how C is partitioned by them (probably outsource this to an algebra system’s cylindrical algebraic decomposition).
3)     Be able to state and prove statements like arg(x)> π/2 & arg(y)> π/2 => log(x*y)=log(x)+log(y)-2 πi.
By hand/unverified computer algebra I have done this by
a.      Log(xy)=Log(x)+Log(y)  (set-valued function identity)
b.      (from 2 above) there are no branch cuts involved in this region
c.      From a sample point, -2 πi is the correct conversion to single-valued.

[Kim Morrison]

I think the question was "what, not directly about branch cuts, do you want to do with such knowledge about branch cuts"?

[Joseph Myers]

The function Complex.arg, coerced to Real.Angle (i.e. eliminating the branch cut and continuous everywhere except 0), is a much better behaved function and much nicer to work with than Complex.arg itself.