Zulip Chat Archive

Stream: general

Topic: FTC and Integration / Differentiation


view this post on Zulip 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?

view this post on Zulip Chris Hughes (Jun 30 2020 at 12:19):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 30 2020 at 14:29):

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

view this post on Zulip Yury G. Kudryashov (Jun 30 2020 at 14:31):

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

view this post on Zulip James Arthur (Jun 30 2020 at 14:45):

I presume that creating an integral like the abf(x)dx \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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 30 2020 at 16:33):

The plan is to use the Lebesgue integral whenever possible.

view this post on Zulip James Arthur (Jun 30 2020 at 16:46):

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

view this post on Zulip Yury G. Kudryashov (Jul 01 2020 at 03:15):

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

view this post on Zulip James Arthur (Jul 01 2020 at 07:56):

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

view this post on Zulip Yury G. Kudryashov (Jul 01 2020 at 07:57):

"Lebesgue integral" = "measure theory integral".

view this post on Zulip Yury G. Kudryashov (Jul 01 2020 at 07:59):

Basically you have some density along the line, then you compute f(x)ρ(x)dx\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 f(x)dμ(x)=f(0)\int f(x)\,d\mu(x)=f(0)).

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jul 01 2020 at 08:01):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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