Simple integral calculations

Stream: Is there code for X?

[Anatole Dedecker]

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]

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

[Benjamin Davidson]

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]

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

[Bryan Gin-ge Chen]

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

[Benjamin Davidson]

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

[Anatole Dedecker]

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

[Benjamin Davidson]

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?

[Mario Carneiro]

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]

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

[Benjamin Davidson]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Benjamin Davidson]

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

[Benjamin Davidson]

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?

[Benjamin Davidson]

@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?

[Johan Commelin]

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

[Benjamin Davidson]

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.

[Heather Macbeth]

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]

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

[Benjamin Davidson]

Heather Macbeth said:

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

I'm satisfied with this solution.

[Benjamin Davidson]

#6216

[Johan Commelin]

@Benjamin Davidson wow, those examples look great!

[Johan Commelin]

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]

Cheers!

[Kevin Buzzard]

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

[Eric Wieser]

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?