Zulip Chat Archive

Stream: maths

Topic: How much of analysis is formalised?


view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 13 2018 at 11:17):

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

view this post on Zulip Chris Hughes (Oct 13 2018 at 11:25):

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.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 13 2018 at 11:29):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 13 2018 at 11:30):

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

view this post on Zulip Chris Hughes (Oct 13 2018 at 11:37):

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.

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 11:46):

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.

view this post on Zulip Johannes Hölzl (Oct 13 2018 at 15:24):

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)

view this post on Zulip Johannes Hölzl (Oct 13 2018 at 15:24):

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

view this post on Zulip Jeremy Avigad (Oct 13 2018 at 15:36):

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

view this post on Zulip Patrick Massot (Oct 13 2018 at 18:52):

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

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 13:20):

@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 R\mathbb{R} to R\mathbb{R} and proof that it is linear (i.e. (f+g)=f+g(f+g)'=f'+g' etc), chain rule, product rule, quotient rule, the derivative of exe^x is exe^x and the derivative of sin(x)\sin(x) is cos(x)\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)\sin(x) is cos(x)\cos(x)? @Chris Hughes am I right in thinking that we still cannot do this in Lean?

view this post on Zulip Chris Hughes (Oct 14 2018 at 13:35):

We can't state it in Lean.

view this post on Zulip Kenny Lau (Oct 14 2018 at 13:39):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 13:42):

the division should go over the subtraction

view this post on Zulip Kenny Lau (Oct 14 2018 at 13:42):

edited

view this post on Zulip Mario Carneiro (Oct 14 2018 at 13:42):

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

view this post on Zulip Kenny Lau (Oct 14 2018 at 13:42):

but it's true because 0/0=0

view this post on Zulip Mario Carneiro (Oct 14 2018 at 13:43):

right, 0 not cos x

view this post on Zulip Kenny Lau (Oct 14 2018 at 13:43):

ah

view this post on Zulip Kenny Lau (Oct 14 2018 at 13:43):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 13:43):

still 0

view this post on Zulip Mario Carneiro (Oct 14 2018 at 13:43):

oh wait

view this post on Zulip Mario Carneiro (Oct 14 2018 at 13:45):

okay that should work

view this post on Zulip Mario Carneiro (Oct 14 2018 at 13:45):

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

view this post on Zulip Kenny Lau (Oct 14 2018 at 13:46):

say that to Patrick Massot

view this post on Zulip Patrick Massot (Oct 14 2018 at 13:52):

What?

view this post on Zulip Kenny Lau (Oct 14 2018 at 13:53):

that's how you defined complex derivative right

view this post on Zulip Patrick Massot (Oct 14 2018 at 13:55):

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

view this post on Zulip Patrick Massot (Oct 14 2018 at 13:55):

not from me

view this post on Zulip Patrick Massot (Oct 14 2018 at 13:55):

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

view this post on Zulip Kenny Lau (Oct 14 2018 at 13:56):

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

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 14:19):

it's one unfold away from sin' = cos

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 14:20):

so we are back to Chris' point.

view this post on Zulip Kenny Lau (Oct 14 2018 at 14:21):

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

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 14:23):

oh, fair point.

view this post on Zulip Sebastien Gouezel (Oct 14 2018 at 16:29):

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

?

view this post on Zulip Reid Barton (Oct 14 2018 at 16:46):

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

view this post on Zulip Johannes Hölzl (Oct 14 2018 at 20:43):

compact_space is surely helpful


Last updated: May 14 2021 at 20:13 UTC