Zulip Chat Archive

Stream: Is there code for X?

Topic: Simple integral calculations


view this post on Zulip Anatole Dedecker (Feb 09 2021 at 08:27):

Now that we have FTC-2, I wanted to discover and experiment a bit with mathlib's integration. I started by calculating some very simple integrals using FTC-2. These are really just direct application of FTC-2 + existing facts on derivative, but I was still suprised not to find e.g ∫ x in a..b, x ^ n inside mathlib. Does it exist somewhere ? Is someone working on proving some classical integrals ? If not, I'd be happy to clean and generalize my proofs and then make a PR

view this post on Zulip Patrick Massot (Feb 09 2021 at 08:50):

I'd be very happy to have those. You should probably coordinate with @Benjamin Davidson.

view this post on Zulip Benjamin Davidson (Feb 09 2021 at 09:00):

I've written a few of these already but had put it on hold due to this discussion in "Whats new in Lean maths" regarding doing them by compute. If they're wanted I'd be glad to work on them.

view this post on Zulip Anatole Dedecker (Feb 09 2021 at 09:16):

Oh I see, I'm late to the party :sweat_smile:

view this post on Zulip Bryan Gin-ge Chen (Feb 09 2021 at 14:11):

Oh, it looks like we never added integral_deriv_eq_sub' and the continuous attribute on continuous_sin from that thread either!

view this post on Zulip Benjamin Davidson (Feb 09 2021 at 21:58):

I can put that together later this week. @Anatole Dedecker would you like to collaborate?

view this post on Zulip Anatole Dedecker (Feb 10 2021 at 08:06):

Yes of course ! I don't have time for Lean today, but I'd be happy to help after that

view this post on Zulip Benjamin Davidson (Feb 14 2021 at 01:46):

I've been working on these and was wondering where they would go once they're ready. For example, does

lemma integral_sin :  x in a..b, sin x = cos a - cos b := sorry

belong in measure_theory.interval_integral (which would require an import), in analysis.special_functions.trigonometric, or somewhere else entirely?

view this post on Zulip Mario Carneiro (Feb 14 2021 at 01:48):

analysis.special_functions.trigonometric contains theorems about measurability of sin, as well as the derivative of sin, so it seems like a good place to put the integral too

view this post on Zulip Mario Carneiro (Feb 14 2021 at 01:49):

Although your theorem looks like a special case of a theorem about antiderivatives with only one cos on the rhs

view this post on Zulip Benjamin Davidson (Feb 14 2021 at 01:54):

Sorry, I'm not sure what you mean by that.

view this post on Zulip Mario Carneiro (Feb 14 2021 at 01:55):

something like deriv g = f -> \int x in a..b, f x = g b - g a

view this post on Zulip Mario Carneiro (Feb 14 2021 at 01:56):

maybe it's not a perfect fit for this lemma, but it should at least make the proof a one-liner

view this post on Zulip Benjamin Davidson (Feb 14 2021 at 01:58):

Oh, I'll be adding a lemma like that. And it does make the proof of integral_sin a one-liner.

view this post on Zulip Benjamin Davidson (Feb 14 2021 at 02:01):

So I will put integrals of special functions in their corresponding files; i.e. integrals of trigonometric functions in analysis.special_functions.trigonometric, integral of exp in analysis.special_functions.exp_log... okay?

view this post on Zulip Benjamin Davidson (Feb 17 2021 at 15:28):

@Mario Carneiro It seems that with #6058 this will no longer be possible, since measure_theory.interval_integral now imports the analysis.special_functions files.
What do you suggest instead?

view this post on Zulip Johan Commelin (Feb 17 2021 at 15:33):

hmm, at first sight I would think that import should be the other way round. Can we reorganise some lemmas?

view this post on Zulip Benjamin Davidson (Feb 17 2021 at 15:38):

That's what I thought, too, hence my plan to import measure_theory.interval_integral into analysis.special_functions.exp_log. But I don't have any idea as to how to possibly resolve this issue.

view this post on Zulip Heather Macbeth (Feb 17 2021 at 15:57):

I think it's rather fundamental. The Bochner integral is now constructed as a special case of L^1 and a special special case of L^p, so powers have to be imported into it.

view this post on Zulip Heather Macbeth (Feb 17 2021 at 15:58):

Perhaps just add a separate file analysis.special_functions.integrals which imports interval_integral.

view this post on Zulip Benjamin Davidson (Feb 17 2021 at 18:18):

Heather Macbeth said:

Perhaps just add a separate file analysis.special_functions.integrals which imports interval_integral.

I'm satisfied with this solution.

view this post on Zulip Benjamin Davidson (Feb 19 2021 at 05:12):

#6216

view this post on Zulip Johan Commelin (Feb 19 2021 at 05:59):

@Benjamin Davidson wow, those examples look great!

view this post on Zulip Johan Commelin (Feb 19 2021 at 06:00):

As long as Lean couldn't do those integrals by itself it looked pretty silly of course. I think this is a very nice milestone!

view this post on Zulip Benjamin Davidson (Feb 19 2021 at 07:51):

Cheers!

view this post on Zulip Kevin Buzzard (Feb 19 2021 at 08:08):

That is great! Many thanks! I'll tell the undergraduates they can do their calculus homework in Lean :-)

view this post on Zulip Eric Wieser (Feb 19 2021 at 08:53):

Presumably you can actually do interactive computation here (i.e. actually do and not just check the homework) by introducing a dummy variable result for the RHS of the statement, and then using norm_num to clean up the left hand side. Is there a less ad-hoc way to do this?


Last updated: May 07 2021 at 22:14 UTC