Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC