## Stream: new members

### Topic: functional analysis

#### Michael R Douglas (Jul 16 2019 at 18:34):

Hello! I am new to this but I have been working through tutorials and the libraries, and I am ready to start a project.
I would like to do something in mathematical physics. My original hope was to start defining perturbative quantum field
theory along the lines of Kevin Costello's book. Or I might try something simpler, like classical mechanics of particles.
My question is, are there any near-term plans to put any functional analysis into mathlib. Even functions from R to R^k and
basic calculus would be enough to do something. I saw the topology definitions, Cauchy sequences and data.complex.exponential.
Are these the foundations that will be used, or is this up for discussion? Has anyone outlined what this would look like ? Thanks!

#### Michael R Douglas (Jul 16 2019 at 18:55):

I just found analysis.normed_space.deriv, will look at that now. But clearly there is a long way to go. Is there a plan?

#### Johan Commelin (Jul 16 2019 at 19:18):

I think @Kevin Sullivan is also working on physics related things.

#### Johan Commelin (Jul 16 2019 at 19:18):

People have worked on the basics of topological/normed vector spaces, Banach spaces, but not much more.

#### Johan Commelin (Jul 16 2019 at 19:18):

I'm not aware of any big road maps

#### Johan Commelin (Jul 16 2019 at 19:19):

@Michael R Douglas Also, welcome! :wave:

#### Kevin Buzzard (Jul 16 2019 at 19:21):

The mathematicians who have been around here the longest are people like me, Patrick and Johan, and none of us are analysts. So algebra and topology have forged ahead, rather leaving analysis behind. Sebastian Gouezel has recently started to put things right, but my understanding is that things are more subtle than one might naively expect. On the other hand there's plenty of analysis in other theorem provers so we just have to catch up.

#### Sebastien Gouezel (Jul 16 2019 at 19:32):

I'm not really an analyst either, but I would love to see some day Fourier transform and Sobolev spaces in Lean!

#### Mario Carneiro (Jul 16 2019 at 19:42):

The Bochner integral is currently under construction, which is where we intend to get multivariate calculus. The derivative is already mostly there, but neither one has been specialized for the real univariate case yet

#### Kevin Buzzard (Jul 16 2019 at 19:54):

and they only work for Cauchy reals ;-)

#### Mario Carneiro (Jul 16 2019 at 20:02):

I may not have been sufficiently clear in the other thread because the point was to talk about transfer what-if scenarios, but I don't think we will ever have Dedekind reals in mathlib. Having multiple versions of a type like real is just asking for confusion and indecision. (Instead, we will show that real acts just like Dedekind reals in whatever way we need.)

Last updated: May 15 2021 at 22:14 UTC