Zulip Chat Archive

Stream: maths

Topic: Request for integral lemmas


view this post on Zulip Yury G. Kudryashov (Jan 25 2020 at 23:06):

Hi @Joe , would it be hard for you to formalize 01f(1x)dx=01f(x)dx\int_0^1 f(1-x)\,dx=\int_0^1 f(x)\,dx and abf(x)dx=(ba)01f(a+t(ba))dt\int_a^b f(x)\,dx=(b-a)\int_0^1 f(a+t(b-a))\,dt with the current state of the library? Actually I need the first one and 201f(x)dx=01f(x/2)dx+01f((x+1)/2)dx2\int_0^1f(x)\,dx=\int_0^1f(x/2)\,dx+\int_0^1f((x+1)/2)\,dx.

view this post on Zulip Mario Carneiro (Jan 25 2020 at 23:47):

this should follow from integration by parts

view this post on Zulip Yury G. Kudryashov (Jan 26 2020 at 00:05):

Wouldn't this proof require more than integrability?

view this post on Zulip Yury G. Kudryashov (Jan 26 2020 at 00:10):

I was thinking about something like {f : α → E} {g : β → E} (c : real) (h : ∀ s : set E, is_open s → volume (f ⁻¹' s) = c * volume (g ⁻¹' s)) : integral f = c * integral g.

view this post on Zulip Yury G. Kudryashov (Jan 26 2020 at 01:12):

BTW, do we have a proof of continuous_on f (Icc a b) → integrable_on f (Icc a b)?

view this post on Zulip Yury G. Kudryashov (Jan 26 2020 at 01:14):

Definitely not in master yet

view this post on Zulip Joe (Jan 26 2020 at 02:07):

I’ll PR this soon.

view this post on Zulip Yury G. Kudryashov (Jan 26 2020 at 02:10):

@Joe Thank you!


Last updated: May 11 2021 at 16:22 UTC