Topic: analysis in Lean
Kevin Buzzard (Oct 11 2019 at 00:31):
@Miguel Raz Guzmán Macedo your question deserves its own thread. What is the state of analysis in Lean nowadays? I remember last year when Imperial's 1st years were beginning to learn some basic analysis I wanted to get them to formalise a proof that a power series was differentiable within its radius of convergence and that its derivative was what it should be. Do we have this yet? I tend to pick up students more interested in algebra because that's much closer to my own area of speciality, and this year I have an MSc student doing more group cohomology, at Xena today people were looking at formalising abelian categories and so on -- tinkering with MSc level algebra. But we still have this black hole with no Cauchy integral formula etc. I have this vague recollection that people with more of an overview than me were discouraging me from getting people to formalise single-variable calculus because it should all be done in far more generality. But on the other hand we had multivariable polynomial rings for a long time and then Chris did the single variable case anyway and as far as I am concerned this was really useful (in algebraic geometry one often works with multivariable polynomial rings with a finite number of variables, and many proofs are done by induction on number of variables e.g. the proof that is Noetherian if is). But I don't have enough of a handle on undergraduate analysis and how it generalises once you're at MSc level to know whether the same arguments imply that one should do single-variable calculus. @Patrick Massot you probably explained all of this to me once before, a year or so ago. What's the situation now? @Sebastien Gouezel you probably also know how all this works.
Mario Carneiro (Oct 11 2019 at 01:08):
I think we should try to do the main theorems of single-variable real calculus, but "naturally generalized" to fit the definitions of derivative and integral currently in mathlib
Mario Carneiro (Oct 11 2019 at 01:09):
A lot of statements don't even generalize that much, e.g. mean value theorem and FTC
Mario Carneiro (Oct 11 2019 at 01:10):
We have working definitions of both integral and derivative now
Mario Carneiro (Oct 11 2019 at 01:11):
I recall Paula working on the univariate derivative, I'm not sure whether that got merged
Mario Carneiro (Oct 11 2019 at 01:13):
The thing about differentiating a power series seems a bit technically subtle, and I would be inclined to wait until we have an application that can guide the form of the statement
Miguel Raz Guzmán Macedo (Oct 11 2019 at 02:33):
Beautiful, thank you very much @Kevin Buzzard . I think I'll start with some Spivak theorems and see what crops up.
Also, am I remembering correclty that @Patrick Massot is the person behind the beautiful script that renders lean code into websites with clickable /hideable Lean code? If I ever give a class, that's how it's gonna look...
Sebastien Gouezel (Oct 11 2019 at 05:36):
What's the situation now? Sebastien Gouezel you probably also know how all this works.
The general derivative of a map
E -> F, as a map from
E to the continuous linear maps from
F, is formalized in
analysis/calculus/deriv.lean, and is called
fderiv_within when restricted to within some subset). When
E is the scalar base field, continuous linear maps from
F are canonically identified with
F (by taking the value at
1), giving rise to the undergrad notion of a derivative. This has not been defined yet in mathlib, and it should be (but not restating the definition from scratch, just using the above identification).
Patrick Massot (Oct 11 2019 at 08:21):
Yes, it's probably a good beginner project to downscale the general theory of differentiable maps to the one-dimensional case.
Last updated: May 06 2021 at 18:20 UTC