How much of analysis is formalised?

Stream: maths

[Abhimanyu Pallavi Sudhir]

How much of analysis is formalised right now? I'm guessing basic calculus -- limits, single-variable stuff, Riemann integrals -- are formalised. What about multivariable, complex analysis (e.g. the complex-analytic proof of the fundamental theorem of algebra), fractional calculus, variational calculus, etc.?

[Chris Hughes]

Integrals are there, but very new, only arrived this week, No derivatives at all as far as I know. Complex analysis is currently very limited, no FTA, look through analysis/complex and you'll get the idea.

[Abhimanyu Pallavi Sudhir]

Just simple Riemann integrals or are Lesbegue, etc. also there?

[Abhimanyu Pallavi Sudhir]

Oh, ok, Lesbegue seems to be there -- analysis/lesbegue_measure.lean

[Chris Hughes]

I haven't looked through it too much, but there's something called lintegral which I'm guessing is lebesgue integral, and something called integral and I don't know what that is.

[Kevin Buzzard]

What is the situation regarding differentiation @Patrick Massot ? I am somehow always confused about whether someone is going to set up a theory of calculus for real-valued functions of one real variable or whether this is somehow all going to be subsumed by some massive multivariable possibly infinite-dimensional normed spaces because this was the correct generality that the theory should be developed in so that's how it has to work.

[Johannes Hölzl]

hm, I see this is a little bit confusing lintegral is actually the lower Lebesgue integral (there might be later a upper Lebesgue integral). It is not the Lebesgue integral into the reals, but it is necessary to define it. My intention is to use this integral to define norms on measurable functions and then define the Bochner integral (which is an integral for functions into a separable Banch space, while the Lebesgue integral is integrating functions into reals)

[Johannes Hölzl]

AFAIK, @Jeremy Avigad wants now to start on multivariate analysis, so also derivative of functions etc.

[Jeremy Avigad]

Yes, I have just gotten started. I'll push to leanprover-community as soon as there is anything worth seeing.

[Patrick Massot]

What is the situation regarding differentiation Patrick Massot? I am somehow always confused about whether someone is going to set up a theory of calculus for real-valued functions of one real variable or whether this is somehow all going to be subsumed by some massive multivariable possibly infinite-dimensional normed spaces because this was the correct generality that the theory should be developed in so that's how it has to work.

My hope was to do the possibly infinite dimensional stuff and deduce the 1-dimensional case, but we'll see what Jeremy does

[Kevin Buzzard]

@Abhimanyu Pallavi Sudhir I think it's worth pointing out the analogy here with the theory of polynomials. Johannes Hoelzl made a big library for polynomials in an arbitrary number of variables, and after that one could argue that "Lean had polynomials". However there were lots of basic facts about polynomials in _one_ variable which we did not have (many of which did not generalise to polynomials in an arbitrary number of variables) and eventually Chris decided to lead the development of a theory of polynomials in one variable https://github.com/leanprover/mathlib/blob/master/data/polynomial.lean which turned out to be useful for my personal work on perfectoid spaces and also indirectly started to guide Mario towards how the theory of modules over a ring should actually be implemented in Lean (which has been an interesting open question for months).

In short -- don't let the fact that people are considering writing some huge library of multivariable calculus stop you developing the basic theory of calculus in one variable. Here are a bunch of things, many of which I believe we don't have, and which will be useful for doing M1M1 in Lean: definition of derivative of a function from $\mathbb{R}$ to $\mathbb{R}$ and proof that it is linear (i.e. $(f+g)'=f'+g'$ etc), chain rule, product rule, quotient rule, the derivative of $e^x$ is $e^x$ and the derivative of $\sin(x)$ is $\cos(x)$. These last few things are maybe not even going to be covered by this general grand plan by experts to develop a theory of multivariable everything, but we're back to the same point: what would a _mathematician_ think when we tell them that we cannot prove that the derivative of $\sin(x)$ is $\cos(x)$? @Chris Hughes am I right in thinking that we still cannot do this in Lean?

[Chris Hughes]

We can't state it in Lean.

[Kenny Lau]

forall x, tendsto (fun h, (sin(x+h)-sin(x))/h) (nbhd 0) (nbhd (cos x))

[Mario Carneiro]

the division should go over the subtraction

[Kenny Lau]

edited

[Mario Carneiro]

also it's not true, because that function has a jump discontinuity at 0

[Kenny Lau]

but it's true because 0/0=0

[Mario Carneiro]

right, 0 not cos x

[Kenny Lau]

ah

[Kenny Lau]

forall x, tendsto (fun h, (sin(x+h)-sin(x)-h*cos(x))/h) (nbhd 0) (nbhd 0)

[Mario Carneiro]

still 0

[Mario Carneiro]

oh wait

[Mario Carneiro]

okay that should work

[Mario Carneiro]

at least, it's a true fact, it looks quite different from $\sin'(x) = \cos(x)$

[Kenny Lau]

say that to Patrick Massot

[Patrick Massot]

What?

[Kenny Lau]

that's how you defined complex derivative right

[Patrick Massot]

I'm not sure what you are talking about, but the definition of complex derivatives in kbb comes from Tom Hales

[Patrick Massot]

not from me

[Patrick Massot]

But it looked ok. Is the discussion around what happens at h=0?

[Kenny Lau]

the discussion is that it looks quite different from sin'(x) = cos(x)

[Kevin Buzzard]

it's one unfold away from sin' = cos

[Kevin Buzzard]

so we are back to Chris' point.

[Kenny Lau]

it isn't because this isn't defining a function

[Kevin Buzzard]

oh, fair point.

[Sebastien Gouezel]

As far as I can see, there is no typeclass for compact spaces, right? (I have the impression that compact is only a predicate on subsets of topological spaces). Is there any problem with

class compact_space (α : Type u) [topological_space α] :=
(compact_univ : compact (univ : set α))

?

[Reid Barton]

I think I suggested an identical definition on zulip a week or two ago. Haven't had much time for actual Lean recently though.

[Johannes Hölzl]

compact_space is surely helpful