segment partitions for integrals

Stream: maths

[Yury G. Kudryashov]

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]

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

[Joe]

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]

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

[Yury G. Kudryashov]

And not every derivative is Lebesgue integrable.

[Kevin Buzzard]

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]

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]

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

[Patrick Massot]

There are many GitHub issues about that.

[Patrick Massot]

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

[Patrick Massot]

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

[Yury G. Kudryashov]

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

[Patrick Massot]

How can that be? You mean very irregular functions?

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

But this has nothing to do with Lebesgue vs Riemann.

[Patrick Massot]

Or am I missing something?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

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]

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

[Bhavik Mehta]

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]

Surprised in which direction?

[Bhavik Mehta]

Haha, surprised that the number for lean was low

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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

[Bhavik Mehta]

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]

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

[Kevin Buzzard]

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]

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

[Bhavik Mehta]

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

[Kevin Buzzard]

Not in the way I want to see it improving

[Kevin Buzzard]

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

[Kevin Buzzard]

I think a lot of these questions are just gimmicks.

[Kevin Buzzard]

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]

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]

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]

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

[Sebastien Gouezel]

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]

How do you do Riemann-Stieltjes with Lebesgue?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Sebastien Gouezel]

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