## Stream: maths

### Topic: Request for integral lemmas

#### Yury G. Kudryashov (Jan 25 2020 at 23:06):

Hi @Joe , would it be hard for you to formalize $\int_0^1 f(1-x)\,dx=\int_0^1 f(x)\,dx$ and $\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 $2\int_0^1f(x)\,dx=\int_0^1f(x/2)\,dx+\int_0^1f((x+1)/2)\,dx$.

#### Mario Carneiro (Jan 25 2020 at 23:47):

this should follow from integration by parts

#### Yury G. Kudryashov (Jan 26 2020 at 00:05):

Wouldn't this proof require more than integrability?

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

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

#### Yury G. Kudryashov (Jan 26 2020 at 01:14):

Definitely not in master yet

#### Joe (Jan 26 2020 at 02:07):

I’ll PR this soon.

#### Yury G. Kudryashov (Jan 26 2020 at 02:10):

@Joe Thank you!

Last updated: May 11 2021 at 16:22 UTC