## Stream: general

### Topic: FTC and Integration / Differentiation

#### James Arthur (Jun 30 2020 at 10:43):

Hi All,

I've decided to formalise some generalised trigonometric functions and more specifically the lower bound of a generalised sinc(x) (sin x /x) function. However, my function is defined as an integral.
$\int_0^x\frac{dt}{(1 - t^p)^\frac{1}{p}}$
I have been told there is a statement of the FTC but not a proof of it, where is it? and how is it used, are there any examples of it?

#### Chris Hughes (Jun 30 2020 at 12:19):

You can get nice formatting if you use double dollar signs, $\int_0^x\frac{dt}{(1 - t^p)^\frac{1}{p}}$.

#### Chris Hughes (Jun 30 2020 at 12:25):

There's a statement of FTC here #1850, but I don't know too much about this part of the library. @Yury G. Kudryashov will know better than me.

#### Yury G. Kudryashov (Jun 30 2020 at 14:29):

I'm in the middle of refactoring integrals in mathlib.

#### Yury G. Kudryashov (Jun 30 2020 at 14:31):

Currently we have no definition of $\int_a^bf(x)\,dx$. We have a definition of $\int f(x)\,d\mu(x)$, and most theorems assume that $\mu$ is the canonical measure. We also have a definition of $\int_{x\in A}f(x)\,d\mu(x)$.

#### James Arthur (Jun 30 2020 at 14:45):

I presume that creating an integral like the $\int_a^b f(x)dx$ is too hard for me to try and create ? But if I was to go about it, would it just be riemann sums? The other definitions look cryptic and maybe not of use to me

#### Chris Hughes (Jun 30 2020 at 14:47):

Probably what will happen is that there will be a cryptic definition, but also a proof that it's the same as a Riemann integral whenever a Riemann integral exists.

#### Yury G. Kudryashov (Jun 30 2020 at 16:33):

The plan is to use the Lebesgue integral whenever possible.

#### James Arthur (Jun 30 2020 at 16:46):

Amazing, that makes sense given the definitions you have already given. You can transfer between a $\int{f(x)d\mu}$ form and a lebesgue relatively easily can't you?

#### Yury G. Kudryashov (Jul 01 2020 at 03:15):

What exactly do you mean by $\int f(x)\,d\mu$?

#### James Arthur (Jul 01 2020 at 07:56):

I was told its a measure theory integral. I was told something along the lines of: $\int{f(x)d\mu} = \int_0^\infty{g(x)dx}$ where $f$ and $g$ are related in some way.

#### Yury G. Kudryashov (Jul 01 2020 at 07:57):

"Lebesgue integral" = "measure theory integral".

#### Yury G. Kudryashov (Jul 01 2020 at 07:59):

Basically you have some density along the line, then you compute $\int_{-\infty}^{\infty}f(x)\rho(x)\,dx$ but the definition works for a measure with no density as well (e.g., if $\mu$ is the dirac measure at zero, then $\int f(x)\,d\mu(x)=f(0)$).

#### James Arthur (Jul 01 2020 at 08:00):

Oh sorry. I just thought it was an integral such that you take the rectangles horizontal instead of vertical. It makes sense why my lecturers moved my interest away from it so quickly.

#### Yury G. Kudryashov (Jul 01 2020 at 08:01):

"rectangles horizontal instead of vertical" is part of the formal definition.

#### James Arthur (Jul 01 2020 at 08:02):

I will have to look up the formal definition as that sounds amazing. Thats not implemented at the moment though, it's something that will be implemented in the future?

#### Yury G. Kudryashov (Jul 01 2020 at 08:06):

This is implemented as a general definition (i.e., for any measure space) but it lacks an interface making it useful for undergraduate calculus.

#### James Arthur (Jul 01 2020 at 08:14):

Thankyou, I'll just have to wait for the integrals to be useful. I doubt I could help formalise any of it.

Last updated: May 10 2021 at 19:16 UTC