## Stream: maths

### Topic: segment partitions for integrals

#### Yury G. Kudryashov (Dec 17 2019 at 18:42):

Hello, I'm thinking about formalizing Riemann/Henstock–Kurzweil/McShane integrals. What would you suggest as a type for partitions? My first draft is

structure MS_partition (a b : ℝ) :=
(n : ℕ)
(endpts : fin (n + 1) → ℝ)
(mem_endpts : ∀ i, endpts i ∈ Icc a b)
(endpts_mono : monotone endpts)
(endpts_0 : endpts 0 = a)
(endpts_n : endpts (fin.last _) = b)
(pts : fin n → ℝ)


Probably we should also have a type for sorted collections of points, i.e. n+endpts+endpts_mono fields from the structure above with operations like "insert a point", "merge two collections".

#### Yury G. Kudryashov (Dec 17 2019 at 18:58):

Would it be better to use {l : list α // sorted l}?

#### Joe (Dec 17 2019 at 19:33):

Is it possible to use the Bochner integral instead? Else we'll have two different notions of integration. And proving they are equivalent (under certain conditions) is not an easy task...
There is such a file in Isabelle, which just goes on and on forever.
http://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Equivalence_Lebesgue_Henstock_Integration.html
@Yury G. Kudryashov

#### Yury G. Kudryashov (Dec 17 2019 at 19:46):

As far as I understand, measure-theoretic integrals are not well-suited for, e.g., integrals over paths in complex.

#### Yury G. Kudryashov (Dec 17 2019 at 19:47):

And not every derivative is Lebesgue integrable.

#### Kevin Buzzard (Dec 17 2019 at 19:56):

These "compatibility proofs" might just be inevitable. At some point we'll need Haar measure on a locally compact topological group and we'll have to prove that it agrees with whatever other integrals there are on the reals at that point

#### Patrick Massot (Dec 17 2019 at 20:28):

Yuri, what kind of functions to you want to integrate over paths in complex? I can't see any application where Lebesgue integral wouldn't be enough. I'm sure one can cook up examples, but it seems very very low on the priority list. We don't even know how to integrate the derivative of a smooth function from reals to reals.

#### Joe (Dec 17 2019 at 20:39):

Sometimes I really hope to have a roadmap or a checklist of things that people want to have in mathlib.

#### Patrick Massot (Dec 17 2019 at 20:40):

There are many GitHub issues about that.

#### Patrick Massot (Dec 17 2019 at 20:40):

But first you can guess that every math taught to 1st students at university should be in.

#### Patrick Massot (Dec 17 2019 at 20:41):

$\int_a^b f'(t)dt = f(b) - f(a)$ is certainly wanted.

#### Yury G. Kudryashov (Dec 17 2019 at 20:41):

1. As far as I understand, integrals dz are hard to formulate with Lebesgue

#### Patrick Massot (Dec 17 2019 at 20:42):

How can that be? You mean very irregular functions?

#### Patrick Massot (Dec 17 2019 at 20:42):

Every course in complex analysis define them using the most naive Riemann or Lebesgue integration.

#### Patrick Massot (Dec 17 2019 at 20:44):

Simply choose a parametrization $\gamma : [0, 1] \to C$ and integrate $f(\gamma(t))\gamma'(t)$ using any integration theory.

#### Patrick Massot (Dec 17 2019 at 20:45):

Of course we'll want to handle this through differential forms anyway.

#### Patrick Massot (Dec 17 2019 at 20:45):

But this has nothing to do with Lebesgue vs Riemann.

#### Patrick Massot (Dec 17 2019 at 20:45):

Or am I missing something?

#### Yury G. Kudryashov (Dec 17 2019 at 20:50):

I'd prefer to have something like Riemann–Stieltjes integral that works for non-differentiable $\gamma$.

#### Yury G. Kudryashov (Dec 17 2019 at 20:51):

1. For Henstock integral, you have $\int_a^bF'(t)\,dt=F(b)-F(a)$ for any differentiable function.

#### Patrick Massot (Dec 17 2019 at 20:52):

Anyway, you can of course work on whatever you find interesting.

#### Kevin Buzzard (Dec 17 2019 at 20:56):

Sometimes I really hope to have a roadmap or a checklist of things that people want to have in mathlib.

Here's my list: https://github.com/kbuzzard/xena/blob/master/many_maths_challenges.txt . Also check the issues, as Patrick says.

#### Yury G. Kudryashov (Dec 17 2019 at 20:57):

Back to the original question, what would you suggest as the type for endpoints: (a) a monotone function from fin n; (b) a sorted list; (c) a multiset with m.sort.nth_le access to elements?
As far as I can see, (a) has a bonus of not having to rewrite on length equality between the set of intervals and the set of marked points. (b) and (c) work better with the current theory.

#### Yury G. Kudryashov (Dec 17 2019 at 20:59):

About a roadmap: what do you think about creating several github "projects" to organize various long-term TODOs?

#### Bhavik Mehta (Dec 17 2019 at 21:00):

I was surprised at Lean's place in the rankings here: http://www.cs.ru.nl/~freek/100/, this could be used as a (hard) checklist I guess

#### Johan Commelin (Dec 17 2019 at 21:00):

Surprised in which direction?

#### Bhavik Mehta (Dec 17 2019 at 21:02):

Haha, surprised that the number for lean was low

#### Kevin Buzzard (Dec 17 2019 at 21:02):

I think those random questions kind of stink. We want to do serious maths, not puzzles.

#### Kevin Buzzard (Dec 17 2019 at 21:02):

I mean they are a measure of something, but I don't think they are a good measure of how mature your prover is.

#### Johan Commelin (Dec 17 2019 at 21:02):

Here's my list: https://github.com/kbuzzard/xena/blob/master/many_maths_challenges.txt . Also check the issues, as Patrick says.

Maybe this can become the Kevin-30 list, as a companion to the Freek-100 list (-;

#### Kevin Buzzard (Dec 17 2019 at 21:03):

I will add more stuff to it! I'd love to make a 100 list which actually reflects things that working mathematicians think about

#### Johan Commelin (Dec 17 2019 at 21:04):

Well, and then you need to keep track of which prover has done what... :grinning:

#### Bhavik Mehta (Dec 17 2019 at 21:05):

I think some of them aren't random questions - briefly looking at the top few, lean doesn't have the pythagorean theorem, the PNT, Godel's incompleteness and impossibility of doubling the cube: I feel like these demonstrate the complexity of the sort of thing you can do in your prover. That said, I agree they're not really useful for what mathematicians tend to think about, but the build up to these results would mean that there's a reasonable API for, eg logic, and Galois theory

#### Patrick Massot (Dec 17 2019 at 21:06):

Don't we have Pythagorean theorem? I'm almost sure we have it.

#### Kevin Buzzard (Dec 17 2019 at 21:07):

95 have been done. In my mind this is a proof that people can do these lists which computer scientists can come up with. Now mathematicians should make a list of stuff which mathematicians use e.g. class group of a number field, and then gaze in amazement as we discover that even though these systems have been around for decades, not one of them has the class group of a number field (apparently), which was something basically invented by Gauss.

#### Kevin Buzzard (Dec 17 2019 at 21:08):

Statements of the Clay Millennium problems are more interesting than getting Lean up that list.

#### Bhavik Mehta (Dec 17 2019 at 21:08):

But getting lean up that list would have the effect of improving mathlib as well

#### Kevin Buzzard (Dec 17 2019 at 21:08):

Not in the way I want to see it improving

#### Kevin Buzzard (Dec 17 2019 at 21:09):

unless you're talking about starting on Fermat's Last Theorem

#### Kevin Buzzard (Dec 17 2019 at 21:09):

I think a lot of these questions are just gimmicks.

#### Kevin Buzzard (Dec 17 2019 at 21:10):

Lean wasn't mentioned on that web page at all until Floris did the cubing the cube question (which he did because it had been observed that none of the provers had done it!). People at the conference we were at asked Freek to add Lean to the list and he asked us to email him which ones had been done in Lean.

#### Kevin Buzzard (Dec 17 2019 at 21:12):

This started a little buzz of interest and some got done, but it's died down now. But the fact that HOL Light and Isabelle-HOL are so high up is in my mind an indication that the questions aren't the right ones. "Define the tangent bundle of a manifold" is something that mathlib got today, and I think that this is basically impossible in Isabelle (or at least the sheaf of sections of it would be, because their logic is not rich enough to do sheaves of rings using type classes).

#### Joe (Dec 17 2019 at 21:13):

I guess by a roadmap I mean a really detailed one, worked out by an expert. Like how to define things with the right level of abstraction, or a rough outline of proof steps.

For example, with the fundamental theorem of calculus, people may disagree about what notion of integration should be used. Or how general should it be, from intervals into reals, or from intervals into Banach spaces.

#### Joe (Dec 17 2019 at 21:19):

So that the work of elaborating the roadmap into a proof is that of a less-expert

#### Sebastien Gouezel (Dec 17 2019 at 21:59):

My 2 cents: Henstock-Kurzweil integral is essentially useless to formalize mathematics, it is a curiosity in itself that has no applications outside of the theory itself. So, as a building block of a tree of everything, it is really a leaf. But it is true that the theory is very cute, so of course go ahead if you want to formalize it! A mistake that was made in Isabelle is that Lebesgue and Kurzweil-Henstock are on the same footage, and some theories are built with one, some theories with the other one, and you need some glue to mix these theories. I would argue strongly against this in mathlib: please, let Lebesgue (i.e., Bochner) integral be the only first-class citizen.

#### Yury G. Kudryashov (Dec 17 2019 at 22:21):

How do you do Riemann-Stieltjes with Lebesgue?

#### Yury G. Kudryashov (Dec 17 2019 at 22:29):

Especially $\int f\,dg$ with vector-valued $g$.

#### Yury G. Kudryashov (Dec 17 2019 at 22:41):

I don't know how to do it for a non-smooth $g$ without a Riemann-style integral (probably my fault), and if I'm going to formalize Riemann-Stieltjes, then adding Henstock-Kurzweil is relatively easy.

#### Sebastien Gouezel (Dec 18 2019 at 07:32):

When g has bounded variation (the most relevant context), then dg is a (vector-valued) measure, and Lebesgue integral works fine (although it has not been formalized in mathlib, we only have the most important case of positive-valued measures).

#### Kevin Buzzard (Dec 18 2019 at 08:33):

I think a lot of these questions are just gimmicks.

I need to roll back on these comments. I just looked through all the questions again and whilst I do feel like some of them are gimmicks, far more than I remembered are genuine mathematics. I'm still of the opinion that these are bad goals to aim for in general (they've mostly been done already in other theorem provers and for the most part they are not things which people use in their day to day work) but they are more respectable mathematics than I implied above -- sorry Freek. Prime Number Theorem (5), Fermat-Euler (10), zeta(2) (14), Fund Thm Calculus (15), four squares theorem (19). Green's Theorem (21), Pythag Triples (23), Leibniz for Pi (26), Ramsey (31), Taylor's Theoerm (35), Brouwer Fixed Point (36), AM/GM (38), Pell (39) [which we say we've done but we haven't really done], the central limit theorem (47), Dirichlet (48) (I thought we had this via mm0?), lHopital (64), the mean value theorem (75) , Fourier series (76), inclusion/exclusion (96) are all respectable mathematics.

I don't think these questions above stink at all, and we don't have any of them (apparently, although of course to a large extent this is because we are weak at basic analysis). I was just remembering some of the sillier ones when I made those comments yesterday.

#### Mario Carneiro (Dec 18 2019 at 08:42):

They are a huge grab bag. The difficulty and areas of mathematics are all over the place

#### Mario Carneiro (Dec 18 2019 at 08:43):

but I think this is a good thing, as it means there is something for everyone

#### Mario Carneiro (Dec 18 2019 at 08:45):

For me the interest in the problems has always been in the library work they generate. The problems are all endpoint theorems, having little direct use in a formal development, but they spawn a bunch of useful lemmas for the library

#### Kevin Buzzard (Dec 18 2019 at 09:12):

The reason for my outburst yesterday is that I think that mathematics can offer a whole lot more far interesting endpoints (like proving the class group of a number field is finite -- this is still undergraduate level in a maths department) which will also spawn a bunch of useful lemmas for the library and which ultimately are aiming much deeper into mathematics. I'd like to reclaim this "100 challenges" thing from the CS people. But I was way too overcritical of Freek's list, it is far less gimmicky than I had remembered it. I think now is the time though to start suggesting mathematical things in areas which those outside mathematics might find harder to understand. For example defining the Tate-Shaferevich group of an elliptic curve over a number field -- stuff which will force people to develop entire theories.

#### Yury G. Kudryashov (Dec 18 2019 at 15:16):

@Sebastien Gouezel Then maybe I'll look into generalizing Lebesgue to the case of a vector-valued measure.

#### Sebastien Gouezel (Dec 18 2019 at 15:27):

Note that a vector valued measure is just an object of the form f dmwhere m is a positive measure and f is a vector-valued function, so if you have the theory of integration for a positive measure you get it right away for any vector valued measure. But of course there is the need for a usable API...

Last updated: May 12 2021 at 08:14 UTC