Single variable complex analysis

Stream: Is there code for X?

[Adrián Doña Mateo]

Hi, I am fourth year undergraduate studying Computer Science and Mathematics at the University of Edinburgh. As my final year project, I decided to contribute to mathlib and so far I've enjoyed learning how to use Lean. From the undergrad math not in mathlib I see that barely any of the complex analysis undergraduate curriculum is formalized. I was wondering whether somebody has tried formalizing this before or, if not, why?

[Ruben Van de Velde]

I think I've seen @Kevin Buzzard mention the lack of complex analysis a few times, but I don't know any more than that

[Kevin Buzzard]

Well, we have the complex numbers as a field, but I'm not sure that anyone has developed the theory of complex analysis. It is definitely worth talking about this. I used to understand the situation with one-variable real analysis well: the argument was that there was no point developing it directly because at some point one would have to do multivariable real analysis. A lot of stuff has since been done, including, I believe, the fundamental theorem of calculus, so one might naively feel that we are in some sense ready to start complex analysis. I might be wrong though.

[Kevin Lacker]

do any of the other math formalization languages have good complex analysis stuff? i wonder if it might be possible to automatically translate their code over

[Kevin Buzzard]

It will almost certainly not be possible to automatically translate any code over, because if this were a thing then it would have been done way before now to translate other stuff over. The filter stuff from topology was I think all taken from Isabelle, but all ported manually.

[Kevin Lacker]

i don't really see why it wouldn't be possible. at least to have it work in conjunction with a human programmer. a lot of the computer language translation stuff will be like, the computer does 95% of the work, but some structures don't quite map and you have to deal with that manually

[Kevin Lacker]

would it be useful to translate code from, say, isabelle to lean, if that was possible?

[Bryan Gin-ge Chen]

There was some recent discussion of translating proofs in this thread.

[Johan Commelin]

If it produces code that can be integrated well into other parts that want to use it... such a translation tool would be awesome. I have no idea how to write such a tool though.

[Kevin Lacker]

it sounds like everyone in that thread is mathematicians rather than programmers

[Johan Commelin]

It's no good to have a complex analysis library in mathlib that uses its own definition of the complex numbers, and its own polynomials, etc...

[Kevin Lacker]

that's right

[Kevin Lacker]

you're never going to get live importing of isabelle code into lean working

[Johan Commelin]

It needs to be integrated and reusable. Afaik, this is a major challenge that hasn't really been solved before

[Kevin Lacker]

the best tools are things like https://github.com/natural/java2python

[Kevin Lacker]

(for this sort of translation)

[Johan Commelin]

Kevin Lacker said:

it sounds like everyone in that thread is mathematicians rather than programmers

Everyone in that thread includes Mario and Jasmin. Two bigshots in formalization-world. Both of them don't know how not to program.

[Kevin Lacker]

well, i just mean nobody brought up the existing tools to translate programmign languages. no offense to anyone intended

[Johan Commelin]

Feel free to experiment. It would be extremely cool if we could get such a tool to work.

[Kevin Lacker]

OK - i'll take a look at some of the other languages here. perhaps some of the formalizations linked from http://www.cs.ru.nl/~freek/100/ would be useful translation targets

[Kevin Buzzard]

The argument given when this comes up is usually of the form "it's not even clear whether one wants to do this because the resulting stuff will not be idiomatic". I am proudly a mathematician though :-)

[Bryan Gin-ge Chen]

It might be worth digging more into @Mario Carneiro 's metamath-mm0-lean stuff.

[Kevin Buzzard]

Talking of translations and Freek 100, one could argue that once we have uniqueness of the reals proved we could in theory translate the metamath proof of PNT (that's a Freek question, right?) into Lean -- but of course the code would be unreadable and not appropriate for mathlib.

[Kevin Lacker]

if you have an unreadable proof for something, and that's the only proof, why not put it in mathlib until you have a better proof for it

[Bryan Gin-ge Chen]

I thought Mario already did an automatic translation of the metamath proof of PNT into Lean using mm0.

[Bryan Gin-ge Chen]

See this thread.

[Johan Commelin]

@Bryan Gin-ge Chen Yes, but it uses a version of log that isn't the one in mathlib. Crucially, it uses a version of real that isn't the one in mathlib. So to get the correct statement, we need to merge Alex's PR on uniqueness of real.

[Kevin Buzzard]

I asked an IC undergraduate to revive the branch. I'm less busy than I was but still more busy than I'll be after a week on Friday, when I can go back to this if the UG hasn't done it.

[Yakov Pechersky]

Java2python and similar tools rely on the existence of an AST representation of the underlying language, and a specifically built translation mechanism. Both java and python are similar in that they're bytecode based languages too, and have very mature interpreters, and many variants (jvm languages for java, ironpython, pypy etc for python)

[Yakov Pechersky]

So a lot of work of python-to-python or java-to-java has also been done

[Yakov Pechersky]

And then one can bring in discussion of compiler generation -- so many actual implementations of C around! gcc, clang, etc

[Yakov Pechersky]

With Lean 3, we have... Lean 3. And as Mario remarked on a separate thread, it's not very clear how Lean can be represented in AST

[Yakov Pechersky]

i'm sure there are more complications than that -- just some thoughts contrasting traditional PLs from theorem PLs

[Yakov Pechersky]

(Jython exists =) )

[Kevin Buzzard]

Independent of this issue (for which the answer is surely ultimately going to be "if you want complex analysis from Isabelle then feel free to manually port") there's the question of whether we're ready to start on this at all. I was trying to say that 2 years ago I had a clear understanding of why I shouldn't be persuading undergraduates to formalise their 1st year real analysis course for mathlib ("it's not general enough"), but now I have a far poorer understanding of whether I should be persuading undergraduates to formalise their 2nd year complex analysis course.

[Kevin Buzzard]

Mathematically I think the issue is the following. One needs to have a good theory of polynomials in one variable to develop some of the theory of polynomials in a finite set of variables, because several of the foundational proofs use induction in the number of variables. Apparently it is less clear that one needs to have a good theory of one variable real analysis before one develops a multivariable theory, because that kind of interaction is perhaps not there so much. What is the story for complex analysis? Certainly a multivariable theory exists, but is it built on top of the one-variable theory or is the one-variable theory just a special case?

[Kevin Buzzard]

Of course there needs to be a specialised theory of integration etc in one dimension. But does it come next, or is there a ton of other stuff which ideally should be done first?

While we're here, someone might want to start thinking about the Jordan curve theorem I guess? Do we have enough to make this a feasible project? Or is the argument that we will only need it for e.g. rectifiable curves, which might be easier? I don't know the foundations of this stuff.

[Heather Macbeth]

Note that analytic functions already exist in great generality thanks to @Sebastien Gouezel
docs#analytic_at
And @Yury G. Kudryashov has been busy lately with the "glue" from formal power series to functions with domain $E^n$ where E is a Banach algebra. #4316

[Heather Macbeth]

@Alex Kontorovich and I have actually been planning to try Goursat's theorem about contours around triangles, basically as a test case. Here's a stub:
https://github.com/leanprover-community/mathlib/tree/triangles

[Kevin Buzzard]

Thanks Heather! My instinct is that the first key missing definition is that of an integral of a holomorphic function along a path, and a goal might be Cauchy's integral formula. I have no feeling for how close we are on this.

[Kevin Buzzard]

Aah! Triangles would be an even better first goal :-)

[Heather Macbeth]

But I say "test case" because of precisely the issue that Kevin mentions: this would eventually lead to holomorphic -> analytic in one variable, but I don't know if there's a more general, non-Goursat argument that does this directly in several variables.

[Kevin Buzzard]

Looking at the code I guess one question that springs to mind is whether we can prove that reparametrising a curve still gives the same integral -- you go along the sides of the triangle at constant speed

[Heather Macbeth]

One other useful link: mathlib has the definition of a holomorphic function, it's just docs#differentiable but with $\mathbb{C}$ as the field!

[Heather Macbeth]

One thing that is independent of all of this, and could be fun for @Adrián Doña Mateo -- checking that docs#differentiable is equivalent to the Cauchy-Riemann equations.

[Heather Macbeth]

And Alex and I can check in in a few days with some thoughts about whether the Goursat stuff is going to go anywhere.

[Johan Commelin]

Heather Macbeth said:

One thing that is independent of all of this, and could be fun for Adrián Doña Mateo -- checking that docs#differentiable is equivalent to the Cauchy-Riemann equations.

That sounds like a very nice first milestone.

[Patrick Massot]

I still think we should first do differential forms and Stokes, and deduce Cauchy from that.

[Kevin Lacker]

Yakov Pechersky said:

With Lean 3, we have... Lean 3. And as Mario remarked on a separate thread, it's not very clear how Lean can be represented in AST

you don't need a Lean AST for this though - you really just need an AST for the other language. because you are free to generate Lean a much more restricted subset of Lean. i think the hardest thing though is that AFAICT some of the fundamental underlying datatypes are handled differently - like in metamath e.g. http://us.metamath.org/mpeuni/areacirc.html you have statements like (𝑡 ∈ ℝ → 𝑡 ∈ ℂ). in Lean IIUC you can't represent that directly because the type system works differently. fundamental datatypes in e.g. java and python aren't compatible with each other either, but you at least have a mapping between the type hierarchy even if they don't quite work the same.

[Heather Macbeth]

Patrick Massot said:

I still think we should first do differential forms and Stokes, and deduce Cauchy from that.

@Patrick Massot I was hoping you would express an opinion :). Regarding this idea, how would you plan to do Stokes to allow for piecewise-continuous boundary? Would this involve developing the theory of manifolds for the piecewise-linear structure groupoid?

[Patrick Massot]

Why piece-wise continuous? How do you integrate on such a path? I think we only need manifolds with boundaries and corners here (this certainly covers triangles).

[Heather Macbeth]

Sorry, I meant piecewise-smooth.

[Patrick Massot]

Ok. What is the issue then? "concave corners"? I guess we can get them after the fact but it will be messy.

[Heather Macbeth]

I think my concerns were unfounded. I was initially worried about whether one would need a manifold-like structure on the boundary itself (here a piecewise-smooth curve). But I suppose what you are saying is that for a manifold with corners, one has stratification of the boundary into pieces which are genuine smooth manifolds, and so integration over the boundary can be defined neatly as a sum of integration over the pieces.

[Patrick Massot]

Yes.

[Heather Macbeth]

Heather Macbeth said:

But I say "test case" because of precisely the issue that Kevin mentions: this would eventually lead to holomorphic -> analytic in one variable, but I don't know if there's a more general, non-Goursat argument that does this directly in several variables.

In another direction -- do you know any answer to this?

[Heather Macbeth]

i.e., an argument "holomorphic implies analytic" that naturally works in several variables (without a prior one-variable argument)?

[Patrick Massot]

I don't see the point of going through Goursat even in dimension 1.

[Heather Macbeth]

Well, it is a nice argument for a novice, which is the point for @Alex Kontorovich :)

[Patrick Massot]

People usually do that because they have a version of Stokes with too strong assumptions and they insist on defining holomorphic functions as complex-differentiable without assuming C¹ in the real sense.

[Patrick Massot]

Sure, I'm only talking from the mathlib point of view. Doing nice exercises is a different question.

[Heather Macbeth]

But so, do you know any argument for several variables that does not involve reducing to the dimension-1 case?

[Heather Macbeth]

By the way, @Adrián Doña Mateo (or others), if you are interested in joining an attempt to do Goursat, it will be 2020-10-23T15:00:00-04:00 at this link:
https://rutgers.zoom.us/j/95310486457?pwd=QW55SzU4NklMeFd6Y3hjKzc3bU1XZz09

[Patrick Massot]

I know almost nothing about complex analysis in several variables, but I think I always saw things deduced from the one-dimensional case.

[Heather Macbeth]

Yes, I think the standard requirement is that the function be continuous, and individually holomorphic in each variable. But this has always seemed odd to me (although I am sure there are good reasons).

[Heather Macbeth]

Is this definition the same as being complex-differentiable? Or am I overlooking something?

[Heather Macbeth]

Patrick Massot said:

I still think we should first do differential forms and Stokes, and deduce Cauchy from that.

Another point about this: One still needs an independent definition of contour integral -- sometimes one wants to integrate around non-closed contours, or self-crossing contours, and so it would be a pain to be restricted only to integrating only over contours of the form "boundary of a domain in $\mathbb{C}$ with boundary and corners".

[Patrick Massot]

Sure.

[Patrick Massot]

But this has nothing to do with the elementary setup. In differential geometry we want to integrate differential forms on chains that are not boundaries.

[Alex Kontorovich]

The approach in introductory texts, eg., Stein-Shakarchi, is to start with the very basic, like integrals over triangles, and see how much mileage one can get from that idea; amazingly, that little lemma can be whittled rather quickly (at least on the human level; we'll see about Lean) all the way up to Cauchy integral representations, analytic functions, etc. So the hope is to take Step 1, and do so now, without waiting for fancier things to be built...? (And also for me to learn more about how this all works...)

[Patrick Massot]

Sure, go for it!

[Mario Carneiro]

Kevin Lacker said:

Yakov Pechersky said:

With Lean 3, we have... Lean 3. And as Mario remarked on a separate thread, it's not very clear how Lean can be represented in AST

you don't need a Lean AST for this though - you really just need an AST for the other language. because you are free to generate Lean a much more restricted subset of Lean. i think the hardest thing though is that AFAICT some of the fundamental underlying datatypes are handled differently - like in metamath e.g. http://us.metamath.org/mpeuni/areacirc.html you have statements like (𝑡 ∈ ℝ → 𝑡 ∈ ℂ). in Lean IIUC you can't represent that directly because the type system works differently. fundamental datatypes in e.g. java and python aren't compatible with each other either, but you at least have a mapping between the type hierarchy even if they don't quite work the same.

Translation from metamath is a "solved problem" at the technical level at this point. You can easily represent (𝑡 ∈ ℝ → 𝑡 ∈ ℂ) in lean, because lean knows about ZFC. It just says t ∈ Real -> t ∈ Complex where Real and Complex have type set Set, that is, classes of ZFC

[Mario Carneiro]

Also, lean has a logical representation of the kind necessary for this kind of translation, and I have been planning (/long delaying) a translation from lean to MM0 along these lines, using the axiomatization of lean defined here

[Mario Carneiro]

translation between programming languages is much simpler than translating between proof languages, because you don't have to care if your translation is correct

[Kevin Lacker]

I was imagining a workflow like, step 1 manually translate some metamath into 500 lines of lean. it 95% works. then you manually go fix up the 25 bugs

[Mario Carneiro]

I have that, except it's 100% not 95%

[Mario Carneiro]

and it's 1 step to 1 line actually

[Kevin Lacker]

i saw https://github.com/digama0/mm0 and the name "mario carneiro" in about a zillion places, but i didnt see specifically a metamath to lean converter

[Kevin Lacker]

why not run this to generate a lean proof of all the rando stuff that's in metamath and not in lean, then? because it would use a wacky definition of "real" instead of the Lean one?

[Mario Carneiro]

mm0-hs from-mm performs wholescale translations from Metamath to MM0 + MMU or MM0 + MMB. This is the best way to obtain a large test set, because set.mm is quite large and advanced.

[Mario Carneiro]

mm0-hs to-lean translates MM0 into Lean source files compatible with mm0-lean. [WIP]

[Mario Carneiro]

actually I should take off the WIP there, it works

[Mario Carneiro]

why not run this to generate a lean proof of all the rando stuff that's in metamath and not in lean, then? because it would use a wacky definition of "real" instead of the Lean one?

I did that

[Mario Carneiro]

The entire set.mm library has been verified using the lean kernel

[Mario Carneiro]

I have used this to fully verify a lean proof of dirichlet's theorem using the metamath library

[Kevin Lacker]

but for example, http://us.metamath.org/mpeuni/basel.html is not in mathlib. (to pick an example that you yourself wrote ;-) )

[Mario Carneiro]

the main limitation for higher level theorems like PNT is to prove the universality of the types involved, which is needed to prove that metamath's reals are isomorphic to lean's reals

[Mario Carneiro]

It's not in mathlib because it's 500000 lines of unreadable stuff and the community doesn't know what to do with it yet

[Mario Carneiro]

it's kind of an all or nothing proposition, if you want the basel problem in lean to be proven using metamath you will need to bring half of the metamath library along with it

[Mario Carneiro]

current plans revolve somehow with having a separate repo that folks can depend on

[Kevin Lacker]

this automatically generated proof, does it use the Metamath types, like the metamath real number definition, all the way through? or if you look at like the top level of the proof, is that using lean style types

[Bryan Gin-ge Chen]

What's missing before we could set up a separate set-mm-lean repo that anyone could import next to mathlib?

[Mario Carneiro]

Mostly a nice CI script, I guess

[Mario Carneiro]

you would need to download set.mm from the git repo, get mm0-hs and run mm0-hs from-mm and mm0-hs to-lean, and then commit the lean files, where they will coexist with a manually curated set of files providing lean shims

[Kevin Lacker]

what would someone do if they wrote some cool new formalization, but it depended on one of the ugly proofs in set-mm-lean - put it in their own repository?

[Mario Carneiro]

leanproject is designed for that, you know

[Mario Carneiro]

despite appearances not all extant lean code is in mathlib

[Mario Carneiro]

Setting that project up hasn't been a high priority for me because I've been busy with completing other parts of the MM0 project but if someone is interested we can get that started

[Bryan Gin-ge Chen]

I'd be happy to help set the CI scripts up. What you've said above might be enough to get me started.

[Mario Carneiro]

There are a lot of low hanging fruit in the shims too. That is all simple but manual work

[Mario Carneiro]

I'll go set up a repo then

[Mario Carneiro]

Also, regarding isabelle to lean: I've been looking into it. The hard part is proof export from isabelle, because it wasn't designed for it and there are no proof objects

[Kevin Lacker]

i'm interested in doing some amount of "simple but manual work" here :smiling_face: I think it would be handy to have a repo for essentially autogenerated and terrible-looking but still valid lean code

[Mario Carneiro]

The basic procedure is to locate a metamath definition, locate the analogous lean definition (or define it), and then prove the isomorphism

[Mario Carneiro]

See https://github.com/digama0/mm0/blob/master/mm0-lean/mm0/set/post.lean, which sets up the basic infrastructure enough to align the concepts of dirichlet's theorem

[Mario Carneiro]

Like this one:

instance nn0.rel_class : rel_class cℕ₀ ℕ :=
{ aset := nn0ex,
  to := λ n, (n:cℕ₀).1,
  to_mem := λ n, (n:cℕ₀).2,
  to_inj := λ m n e, nat.cast_inj.1 (subtype.eq e),
  to_surj := λ x h, begin
    refine nn0ind' _ h ⟨0, rfl⟩ _,
    rintro _ h ⟨n, rfl⟩, exact ⟨n+1, rfl⟩
  end }

This is proving that cℕ₀, which is notation for metamath's NN0 (natural numbers with zero), is isomorphic to ℕ (lean's nat), using metamath theorems nn0ex which says cℕ₀ is a set, and nn0ind' which is one version of an induction theorem for nn0

[Mario Carneiro]

it also declares it as an instance so that later proofs can use the isomorphism to prove for example that metamath's c0 is mapped to lean's 0 : nat by this isomorphism

[Kevin Lacker]

hmm, interesting. i was imagining pushing down the mapping so that the formulas would be using Lean nat in a bunch of places, and then maybe some axioms would be missing

[Mario Carneiro]

that part happens mostly automatically using the typeclasses, this is the setup

[Mario Carneiro]

But you can't use lean nat directly and get 100% coverage

[Mario Carneiro]

or at least, not without more complex translation

[Mario Carneiro]

However it does use lean's forall, exists, and, or directly, which makes a lot of things easier since you can just definitionally reduce things to see the lean versions

[Mario Carneiro]

But keep in mind that the lean file exporter has no actual knowledge or integration with the lean executable, so its ability to produce nice lean files is extremely limited

[Mario Carneiro]

remember that even lean doesn't know how to print lean terms in a completely 100% faithful way

[Kevin Lacker]

I have empathy for lean's difficulties here, there are like dozens of unicode arrows that mean different things

[Mario Carneiro]

so the role of these shim files is to put notations on things, unfold definitions as required, and basically make the library more human accessible

[Yury G. Kudryashov]

AFAIR, triangles allow us to prove that a complex differentiable is analytic while the general Stokes formula needs continuous differentiability.

[Heather Macbeth]

Indeed, I think Patrick was addressing that point here:

Patrick Massot said:

I don't see the point of going through Goursat even in dimension 1.

Patrick Massot said:

People usually do that because they have a version of Stokes with too strong assumptions and they insist on defining holomorphic functions as complex-differentiable without assuming C¹ in the real sense.

[Heather Macbeth]

(But I didn't quite understand what he was proposing -- is there a version of Stokes requiring less regularity?)

[Johan Commelin]

I learnt last year that there is an old book by Whitney that has extremely general versions of Stokes. But that's all I know.

[Johan Commelin]

I'm very far from an expert.

[Johan Commelin]

With extremely general, I mean: very weak conditions on how differentiable you are, and your manifold is also allowed to be pretty wild.

[Reid Barton]

I can integrate $dx$ along any path $\gamma : [0, 1] \to \mathbb{R^2}$. Doesn't even have to be continuous :upside_down:

[Yury G. Kudryashov]

I think that if Goursat gives us, e.g., the maximum principle before we define differential forms etc, then it's worth it.

[Patrick Massot]

Yes I meant there are versions of Stokes that assume only stuff you get for complex differentiable functions.

[Patrick Massot]

See https://link.springer.com/article/10.1007/BF03024304

[Yury G. Kudryashov]

Thanks a lot for the link!