# Zulip Chat Archive

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

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

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

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