functional analysis

Stream: new members

[Michael R Douglas]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

I'm not aware of any big road maps

[Johan Commelin]

@Michael R Douglas Also, welcome! :wave:

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

and they only work for Cauchy reals ;-)

[Mario Carneiro]

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