## Stream: maths

### 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 $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 (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 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 (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