analysis in Lean

Stream: maths

[Kevin Buzzard]

@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 $R[X_1,X_2,\ldots,X_n]$ is Noetherian if $R$ 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]

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]

A lot of statements don't even generalize that much, e.g. mean value theorem and FTC

[Mario Carneiro]

We have working definitions of both integral and derivative now

[Mario Carneiro]

I recall Paula working on the univariate derivative, I'm not sure whether that got merged

[Mario Carneiro]

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]

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]

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 E to F, is formalized in analysis/calculus/deriv.lean, and is called fderiv(and fderiv_within when restricted to within some subset). When E is the scalar base field, continuous linear maps from E to 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]

Yes, it's probably a good beginner project to downscale the general theory of differentiable maps to the one-dimensional case.