Zulip Chat Archive

Stream: Is there code for X?

Topic: Single variable complex analysis


view this post on Zulip Adrián Doña Mateo (Oct 21 2020 at 15:37):

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?

view this post on Zulip Ruben Van de Velde (Oct 21 2020 at 15:41):

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

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 15:44):

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.

view this post on Zulip Kevin Lacker (Oct 21 2020 at 15:58):

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

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 16:00):

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.

view this post on Zulip Kevin Lacker (Oct 21 2020 at 16:06):

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

view this post on Zulip Kevin Lacker (Oct 21 2020 at 16:07):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 21 2020 at 16:10):

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

view this post on Zulip Johan Commelin (Oct 21 2020 at 16:11):

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.

view this post on Zulip Kevin Lacker (Oct 21 2020 at 16:12):

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

view this post on Zulip Johan Commelin (Oct 21 2020 at 16:12):

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...

view this post on Zulip Kevin Lacker (Oct 21 2020 at 16:12):

that's right

view this post on Zulip Kevin Lacker (Oct 21 2020 at 16:12):

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

view this post on Zulip Johan Commelin (Oct 21 2020 at 16:12):

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

view this post on Zulip Kevin Lacker (Oct 21 2020 at 16:13):

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

view this post on Zulip Kevin Lacker (Oct 21 2020 at 16:13):

(for this sort of translation)

view this post on Zulip Johan Commelin (Oct 21 2020 at 16:13):

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.

view this post on Zulip Kevin Lacker (Oct 21 2020 at 16:13):

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

view this post on Zulip Johan Commelin (Oct 21 2020 at 16:14):

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

view this post on Zulip Kevin Lacker (Oct 21 2020 at 16:16):

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

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 16:16):

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 :-)

view this post on Zulip Bryan Gin-ge Chen (Oct 21 2020 at 16:18):

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

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 16:18):

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.

view this post on Zulip Kevin Lacker (Oct 21 2020 at 16:20):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 21 2020 at 16:20):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 21 2020 at 16:20):

See this thread.

view this post on Zulip Johan Commelin (Oct 21 2020 at 16:25):

@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.

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 16:28):

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.

view this post on Zulip Yakov Pechersky (Oct 21 2020 at 16:41):

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)

view this post on Zulip Yakov Pechersky (Oct 21 2020 at 16:41):

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

view this post on Zulip Yakov Pechersky (Oct 21 2020 at 16:42):

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

view this post on Zulip Yakov Pechersky (Oct 21 2020 at 16:42):

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

view this post on Zulip Yakov Pechersky (Oct 21 2020 at 16:44):

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

view this post on Zulip Yakov Pechersky (Oct 21 2020 at 16:46):

(Jython exists =) )

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 16:46):

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.

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 16:49):

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?

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 16:51):

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.

view this post on Zulip Heather Macbeth (Oct 21 2020 at 16:51):

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 EnE^n where E is a Banach algebra. #4316

view this post on Zulip Heather Macbeth (Oct 21 2020 at 16:52):

@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

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 16:53):

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.

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 16:54):

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

view this post on Zulip Heather Macbeth (Oct 21 2020 at 16:54):

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.

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 16:55):

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

view this post on Zulip Heather Macbeth (Oct 21 2020 at 16:55):

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

view this post on Zulip Heather Macbeth (Oct 21 2020 at 16:56):

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.

view this post on Zulip Heather Macbeth (Oct 21 2020 at 16:56):

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

view this post on Zulip Johan Commelin (Oct 21 2020 at 17:06):

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.

view this post on Zulip Patrick Massot (Oct 21 2020 at 17:20):

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

view this post on Zulip Kevin Lacker (Oct 21 2020 at 17:22):

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.

view this post on Zulip Heather Macbeth (Oct 21 2020 at 19:41):

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?

view this post on Zulip Patrick Massot (Oct 21 2020 at 19:43):

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).

view this post on Zulip Heather Macbeth (Oct 21 2020 at 19:44):

Sorry, I meant piecewise-smooth.

view this post on Zulip Patrick Massot (Oct 21 2020 at 19:46):

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

view this post on Zulip Heather Macbeth (Oct 21 2020 at 19:47):

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.

view this post on Zulip Patrick Massot (Oct 21 2020 at 19:47):

Yes.

view this post on Zulip Heather Macbeth (Oct 21 2020 at 19:47):

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?

view this post on Zulip Heather Macbeth (Oct 21 2020 at 19:48):

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

view this post on Zulip Patrick Massot (Oct 21 2020 at 19:50):

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

view this post on Zulip Heather Macbeth (Oct 21 2020 at 19:51):

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

view this post on Zulip Patrick Massot (Oct 21 2020 at 19:51):

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.

view this post on Zulip Patrick Massot (Oct 21 2020 at 19:52):

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

view this post on Zulip Heather Macbeth (Oct 21 2020 at 19:53):

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

view this post on Zulip Heather Macbeth (Oct 21 2020 at 19:57):

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

view this post on Zulip Patrick Massot (Oct 21 2020 at 19:58):

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

view this post on Zulip Heather Macbeth (Oct 21 2020 at 19:59):

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).

view this post on Zulip Heather Macbeth (Oct 21 2020 at 20:00):

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

view this post on Zulip Heather Macbeth (Oct 21 2020 at 20:25):

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 C\mathbb{C} with boundary and corners".

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:25):

Sure.

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:26):

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.

view this post on Zulip Alex Kontorovich (Oct 21 2020 at 21:13):

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...)

view this post on Zulip Patrick Massot (Oct 21 2020 at 21:18):

Sure, go for it!

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:20):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:22):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:23):

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

view this post on Zulip Kevin Lacker (Oct 21 2020 at 22:24):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:24):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:24):

and it's 1 step to 1 line actually

view this post on Zulip Kevin Lacker (Oct 21 2020 at 22:25):

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

view this post on Zulip Kevin Lacker (Oct 21 2020 at 22:25):

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?

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:26):

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.

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:26):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:26):

actually I should take off the WIP there, it works

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:27):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:27):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:28):

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

view this post on Zulip Kevin Lacker (Oct 21 2020 at 22:28):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:29):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:30):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:30):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:31):

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

view this post on Zulip Kevin Lacker (Oct 21 2020 at 22:32):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 21 2020 at 22:33):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:33):

Mostly a nice CI script, I guess

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:35):

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

view this post on Zulip Kevin Lacker (Oct 21 2020 at 22:35):

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?

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:35):

leanproject is designed for that, you know

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:36):

despite appearances not all extant lean code is in mathlib

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:39):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 21 2020 at 22:39):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:40):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:41):

I'll go set up a repo then

view this post on Zulip Mario Carneiro (Oct 21 2020 at 22:42):

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

view this post on Zulip Kevin Lacker (Oct 21 2020 at 22:46):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 23:09):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 23:09):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 23:12):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 23:14):

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

view this post on Zulip Kevin Lacker (Oct 21 2020 at 23:15):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 23:15):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 23:16):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 23:16):

or at least, not without more complex translation

view this post on Zulip Mario Carneiro (Oct 21 2020 at 23:17):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 23:18):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 23:19):

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

view this post on Zulip Kevin Lacker (Oct 21 2020 at 23:20):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 23:21):

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

view this post on Zulip Yury G. Kudryashov (Oct 22 2020 at 15:26):

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

view this post on Zulip Heather Macbeth (Oct 22 2020 at 17:04):

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.

view this post on Zulip Heather Macbeth (Oct 22 2020 at 17:05):

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

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:08):

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.

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:08):

I'm very far from an expert.

view this post on Zulip Johan Commelin (Oct 22 2020 at 17:09):

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

view this post on Zulip Reid Barton (Oct 22 2020 at 17:10):

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

view this post on Zulip Yury G. Kudryashov (Oct 22 2020 at 18:44):

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

view this post on Zulip Patrick Massot (Oct 22 2020 at 19:34):

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

view this post on Zulip Patrick Massot (Oct 22 2020 at 19:37):

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

view this post on Zulip Yury G. Kudryashov (Oct 22 2020 at 20:57):

Thanks a lot for the link!


Last updated: May 07 2021 at 23:11 UTC