Request for integral lemmas

Stream: maths

[Yury G. Kudryashov]

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]

this should follow from integration by parts

[Yury G. Kudryashov]

Wouldn't this proof require more than integrability?

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

Definitely not in master yet

[Joe]

I’ll PR this soon.

[Yury G. Kudryashov]

@Joe Thank you!