Stream: Is there code for X?
Topic: Simple integral calculations
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
Patrick Massot (Feb 09 2021 at 08:50):
I'd be very happy to have those. You should probably coordinate with @Benjamin Davidson.
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.
Anatole Dedecker (Feb 09 2021 at 09:16):
Oh I see, I'm late to the party :sweat_smile:
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!
Benjamin Davidson (Feb 09 2021 at 21:58):
I can put that together later this week. @Anatole Dedecker would you like to collaborate?
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
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
measure_theory.interval_integral (which would require an import), in
analysis.special_functions.trigonometric, or somewhere else entirely?
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
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
Benjamin Davidson (Feb 14 2021 at 01:54):
Sorry, I'm not sure what you mean by that.
Mario Carneiro (Feb 14 2021 at 01:55):
deriv g = f -> \int x in a..b, f x = g b - g a
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
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.
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
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
What do you suggest instead?
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?
Benjamin Davidson (Feb 17 2021 at 15:38):
That's what I thought, too, hence my plan to import
analysis.special_functions.exp_log. But I don't have any idea as to how to possibly resolve this issue.
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.
Heather Macbeth (Feb 17 2021 at 15:58):
Perhaps just add a separate file
analysis.special_functions.integrals which imports
Benjamin Davidson (Feb 17 2021 at 18:18):
Heather Macbeth said:
Perhaps just add a separate file
I'm satisfied with this solution.
Benjamin Davidson (Feb 19 2021 at 05:12):
Johan Commelin (Feb 19 2021 at 05:59):
@Benjamin Davidson wow, those examples look great!
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!
Benjamin Davidson (Feb 19 2021 at 07:51):
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 :-)
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