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

belong in 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):

something like 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 exp in analysis.special_functions.exp_log... okay?

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

#### 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 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 (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 interval_integral.

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

#6216

#### 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!

Cheers!

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