integrating on a piecewise differentiable curve

Stream: Is there code for X?

[Alex Kontorovich]

I want to define the complex logarithm. It takes a domain $\Omega$ (open, connected, simply connected subset of $\mathbb C$) which does not contain $0$, and a choice of base point $z_0\in\Omega$, and for an argument $z\in\Omega$, outputs $\int_\gamma \frac{dw}{w}$, where $\gamma$ is a piecewise differentiable curve from $z_0$ to $z$. (It has to be proved that the definition is independent of the choice of $\gamma$.) Question: do we already have some API for piecewise differentiable curves? The input should be an interval $[a,b]$, $n : \N$, and $a=x_0<x_1<...<x_n=b$, and $\gamma$ (which is really an equivalence class of parametrizations) is continuously differentiable on each $[x_i,x_{i+1}]$. Any pointers for how to do this are very welcome, thanks!

[Patrick Massot]

You need to use two $ signs to enclore LaTeX formulas.

[Patrick Massot]

And you can have a look at how your question is handled in Isabelle that has a huge library about integrating on curves in $\mathbb C$.

[Alex Kontorovich]

ok great, thanks; so I think that answers my question in that it sounds like this doesn't already exist in mathlib? (But great idea to see how it was implemented elsewhere)

[Yury G. Kudryashov]

Another option: you consider docs#Complex.exp as a covering and lift a path.

[Kalle Kytölä]

When @Vincent Beffara proved (at least most of) the Riemann mapping theorem (in Lean3), we discussed this with him quite extensively. I think one should definitely prove that all holomorphic functions have primitives in simply connected domains ($\frac{f'(z)}{f(z)}$ for non-vanishing $f$ is an important special case, of course). For convex and star-shaped domains, Vincent had this (if I remember correctly), but it seemed slightly nontrivial to decide in which form the statement should go to mathlib.

The specific awkward thing is that one wants to define simply connectedness in terms of $C^0$ paths, but integration is a priori defined along piecewise-$C^1$ paths. Vincent suggested (and I like the strategy very much) that one could first have that $f(z) \mathrm{d}z$ is a closed 1-form when $f$ is holomorphic (and is exact when $f$ has a primitive), and then use Poincaré lemma to make it locally exact, and then define integrals along any $C^0$-paths using finite subdivisions and local primitives (from local exactness) --- and of course check that the result is $C^0$-homotopy-invariant. We also thought the right generality might involve doing the same not just for 1-forms but also $n$-forms (which can also a priori be integrated only along $C^1$ submanifolds of dimension $n$). Of course the status of cotangent bundles in Mathlib makes this difficult to do right now...

(For the current formulation of the formalization of the RMT, simply connectedness was temporarily defined as "every nonvanishing holomorphic function has a square root", but this is of course another special case of the same general thing that the existence of logarithm is about.)