antiderivative

Stream: Is there code for X?

[Johan Commelin]

https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets claims we already have antiderivatives. Which declaration should we link to? I've never used this part of mathlib myself.

[Yury G. Kudryashov]

We have theorems about λ b, ∫ x in a..b, f x

[Yury G. Kudryashov]

We don't define "antiderivative"; we use has_deriv(_within)_at instead.

[Yury G. Kudryashov]

One can define def is_antideriv_on (f f' : real → E) (s : set real) := ∀ x ∈ s, has_deriv_at (f x) (f' x) but many theorems (e.g., FTC-*) have versions with weaker assumptions.

[Yury G. Kudryashov]

Possibly, we should indeed create a file somewhere in src with definitions from standard university course that should never be used in mathlib (unless we decide otherwise) and explanations about the mathlib way to say the same.

[Yury G. Kudryashov]

Or put it outside of src but generate docs for this file.

[Patrick Massot]

Yes, I think we can have declaration that are used as targets from this list. They would still give entry points.

[Johan Commelin]

Would it be bad to just link to has_deriv_at?

[Alex]

I'm sorry to bump a two-week-old topic, but if I may,
...how is formal integration a trivial undergrad todo target at all?
I'm talking about https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets...

It's been only 50 years since Risch's proof that the problem can be approached algorithmically, and we still don't have a complete implementation of what he's outlined in his 70's works.

Only pure transcendental case of Risch's algorithm is more or less widely known and received several major implementations. The further we stray away from it into the arcane world of algebraic differential field extensions, the worse the modern CASes perform.

Stating that f is the antiderivative for g is somewhat trivial, checking it less so, but usually doable if we choose the right differential field extension tower to work with; checking if a function has an antiderivative in given field or its liouvillian extension is by no means a trivial task...

[Alex J. Best]

The undergraduate TODO list is based on the French curriculum https://media.devenirenseignant.gouv.fr/file/agreg_externe/59/7/p2020_agreg_ext_maths_1107597.pdf, so all points on the list should be interpreted as having the same level of material in Lean that is taught in one of these undergraduate classes in a mathematics bachelors degree. I don't know to many that teach Risch's algorithm and certainly none give the full details so thats out of scope for this TODO. Instead the TODO is about simpler integrals and the theory behind them

[Alex]

so not the algorithm, but a common bunch of recipes?

[Alex]

like just what they usually give to first year students, not necessarily math majors?

[Alex J. Best]

and we already have some nice examples in https://github.com/leanprover-community/mathlib/blob/master/test/integration.lean and https://github.com/leanprover-community/mathlib/blob/master/test/differentiable.lean

[Alex J. Best]

The list is based on a full bachelor degree, so the whole list is about what the equivalent of math majors should know, but some material is taught in the first year

[Alex]

I see. Risch's algo uses way more. Can hardly imagine an undergrad approaching it. Also takes knowledge from several distinct fields of maths.

So the goal is to have a framework such that we can verify that F is indeed the antiderivative for f,
given both F and f?

(in France they say primitive function I think?)

[Alex]

Also while we're at it, you linked the first file integration.lean.

The following section

/- inverse -/
example : ∫ x : ℝ in 2..3, x⁻¹ = log (3 / 2) := by norm_num

should be renamed to reciprocal I believe. The inverse of sin(x) is arcsin(x), not 1/sin(x) :)

[Alex]

I remember they said in lean faq that they don't like pullrequests, so perhaps that should be done by someone who holds the authority :)

[Alex J. Best]

Well this is in mathlib! Not the core of Lean, we love pull requests and merge 10-20 a day https://github.com/leanprover-community/mathlib/pulls. That said, the name for the function ⁻¹ is inv in lean so I don't think its so bad to call that section inverse

[Alex]

I trust there was reason for calling it that. Just saying that it will be confusing to people outside Lean.
Mathematicians call 1/f the reciprocal, to specifically distinguish the two notions of inverse.
Moreover, it's a common translation mistake when the original text was in one of the languages where there is no distinct term for reciprocals.

[Alex]

I'm not sure if I should make a pull request over such a little detail. Would probably look like nitpicking. But have to say that that particular misuse of the term irritates a bit :)

[Alex]

I wonder how far is mathlib currently from proving Liouville's Theorem

[Kevin Buzzard]

I suspect that it's in scope but as far as I know nobody is working on it. Is it done in any of the other provers e.g. Coq?

[Johan Commelin]

@Alex If you want to change inverse to reciprocal it would have to be done throughout mathlib consistently.

[Johan Commelin]

And one immediate tricky thing is that you would need an abbreviation, like inv abbreviates inverse. But rec is already used all over the place for recursor.

[Alex]

Kevin Buzzard said:

I suspect that it's in scope but as far as I know nobody is working on it. Is it done in any of the other provers e.g. Coq?

Not sure. Probably not. I'm not an expert on the subject, sorry. I currently learn about formal integration the way Risch approached it, in my spare time, as a hobby. I take it slowly, as work and life eats most of my time, and I still have a long way to go.

Liouville's theorem takes a few lectures of a postgraduate computer algebra course to prove even in special (non-general) form, with very little details and starting with the field of complex numbers rather than the rationals. A full-fledged proof will take quite some effort.

[Alex]

But it will of course depend on the amount of machinery already available. And I'm VERY new to Lean, literally zero knowledge yet. Can't estimate at all.

[Alex]

Johan Commelin said:

Alex If you want to change inverse to reciprocal it would have to be done throughout mathlib consistently.

I'm not sure this is a good idea. Is there no possibility for 1/f syntax for reciprocals? $\sin^{-1} x$ on the other hand usually denotes the arcsine rather than the cosecant.

[Alex]

Kevin Buzzard said:

I suspect that it's in scope but as far as I know nobody is working on it. Is it done in any of the other provers e.g. Coq?

Its value is in proving that a function has no elementary integral, when it does not.
Basically it says "an elementary antiderivative from differential field K can always be expressed as a linear combination* of logarithms of functions from K plus some function from K", asterisk saying "coefficients come from $\overline{K}$, i.e. algebraic closure of K". Then, with some transforms, one shows for example, that no function of such form could yield the integrand, thus proving the antiderivative to be non-elementary.

But I somehow suspect even the proofs that certain functions are not elementary to be out of reach yet for theorem provers. Yet. I am glad to see them improving and growing rapidly recently.

[David Wärn]

Alex said:

I'm not sure this is a good idea. Is there no possibility for 1/f syntax for reciprocals? $\sin^{-1} x$ on the other hand usually denotes the arcsine rather than the cosecant.

Apparently in mathlib (1/sin)(x), sin⁻¹ x, (sin x)⁻¹ and 1/(sin x) all mean the same thing. You can use whichever one you like. I don't think we have any special notation for arcsin. The thing to keep in mind is that mathlib's notation is designed to be very general. The common practice of writing $\sin^2(x)$ and $\sin^{-1}(x)$ to mean completely different things doesn't translate very well.

[Alex]

David Wärn said:

Alex said:

I'm not sure this is a good idea. Is there no possibility for 1/f syntax for reciprocals? $\sin^{-1} x$ on the other hand usually denotes the arcsine rather than the cosecant.

Apparently in mathlib (1/sin)(x), sin⁻¹ x, (sin x)⁻¹ and 1/(sin x) all mean the same thing. You can use whichever one you like. I don't think we have any special notation for arcsin. The thing to keep in mind is that mathlib's notation is designed to be very general. The common practice of writing $\sin^2(x)$ and $\sin^{-1}(x)$ to mean completely different things doesn't translate very well.

Oh you're so very right.
The culprit is the $\cos^2(x)$ of course, which is, to quote one of the mathematicians, "no sane mind shall interpret as anything other than $\cos(\cos(x))$". Unfortunately, people have grown too used to writing $\cos^2$ to just declare it illegal.

[Kevin Buzzard]

But I somehow suspect even the proofs that certain functions are not elementary to be out of reach yet for theorem provers. Yet. I am glad to see them improving and growing rapidly recently.

I think you're wrong. I read some of this stuff about a decade ago and I don't see any obstruction to doing this in Lean, other than the standard obstruction we have in our area, which is that there is so much to do and too few people to do it. Note that we proved insolvability of the quintic which is in some sense a similar problem.

[Alex]

Kevin Buzzard said:

But I somehow suspect even the proofs that certain functions are not elementary to be out of reach yet for theorem provers. Yet. I am glad to see them improving and growing rapidly recently.

I think you're wrong. I read some of this stuff about a decade ago and I don't see any obstruction to doing this in Lean, other than the standard obstruction we have in our area, which is that there is so much to do and too few people to do it. Note that we proved insolvability of the quintic which is in some sense a similar problem.

I'm glad to be wrong here. Yes indeed I was mostly implying that performing it takes very specific knowledge and therefore a very rare specialist to do it. I don't doubt that there's no theoretical obstacle or some insurmountable spike of proof complexity.

Proving that a general quintic is insoluble in radicals can indeed be considered a milestone. A good showcase for galois theory. But the result is more well-known, so there probably are much more people who'll readily understand it.

[Alex]

By the way, are there people whom I might ask about differential algebra, formal integration, etc, in this chat? I promise I won't have too many questions :)

[Johan Commelin]

@Alex Feel free to ask, probably best in the #maths stream. But we can't promise answers :wink:

[Patrick Massot]

Alex said:

I'm sorry to bump a two-week-old topic, but if I may,
...how is formal integration a trivial undergrad todo target at all?
I'm talking about https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets...

It's been only 50 years since Risch's proof that the problem can be approached algorithmically,

The issue is that are interpreting those lines in a completely different way from the intended meaning. Nobody is talking about an algorithmic approach to computing antiderivatives here. Here we only want to prove that continuous functions from real numbers to real numbers have antiderivatives. mathlib already have a much more general result so the trivial TODO is to deduce the elementary version. mathlib is primarily about proving stuff, not computing, although ideally it could do both.

[Yury G. Kudryashov]

Implementing the algorithm (as a tactic, with proofs) would be nice too but it's much harder.

[Yury G. Kudryashov]

I'd love simp (or integrate or whatever) to simplify non-trivial integrals without any hints.