## Stream: maths

### Topic: interval_integrable.comp

#### Benjamin Davidson (Apr 05 2021 at 07:52):

I have currently proved the following:

import analysis.special_functions.integrals
open measure_theory
variables {a b : ℝ} {f g : ℝ → ℝ} {μ : measure ℝ} [locally_finite_measure μ]

lemma interval_integrable.comp (hf : continuous f) (hg : continuous g) :
interval_integrable (λ x, (f ∘ g) x) μ a b :=
(hf.comp hg).interval_integrable a b


How can I improve this lemma? Namely, how can I prove it using assumptions about integrability rather than assumptions about continuity?

Thanks!

#### Mario Carneiro (Apr 05 2021 at 07:54):

For one thing, generalize from real to any space with the appropriate properties

#### Damiano Testa (Apr 05 2021 at 07:56):

I do not know much about the integrability part of mathlib, but a and b simply seem to stand in to identify a subset over which you integrate. It may be possible to integrate over a subset of a measurable space, I imagine...

#### Mario Carneiro (Apr 05 2021 at 08:01):

There are a bunch of theorems in interval_integral about composition with various linear functions but I didn't see anything about arbitrary composition. I think this usually goes by the name "integration by substitution"

#### Mario Carneiro (Apr 05 2021 at 08:01):

or integration on a preimage measure

#### Mario Carneiro (Apr 05 2021 at 08:09):

the only relevant theorem I could find is docs#measure_theory.integrable_map_measure

#### Mario Carneiro (Apr 05 2021 at 08:11):

oh, docs#measure_theory.set_integral_map seems to be a bit closer

#### Benjamin Davidson (Apr 05 2021 at 11:57):

Yes, but here I am not trying to actually integrate the composition of functions (something else I am working on) but trying to show the integrability of the composition of two integrable functions...due to my own lack of understanding I'm not sure if that impacts what you are saying @Mario Carneiro

#### Mario Carneiro (Apr 05 2021 at 12:10):

Those two should be basically the same thing

#### Benjamin Davidson (Apr 05 2021 at 14:47):

Ah, then perhaps it’s best I wait until I complete the “integration by substitution” stuff...I know that @Anatole Dedecker is also working on a more general “change of variable” lemma

#### Benjamin Davidson (Apr 05 2021 at 14:49):

Am I correct, though, that I should just be able to assume that the functions are interval integrable, not continuous?

#### Damiano Testa (Apr 05 2021 at 14:57):

I do not think that the composite of two Riemann/Lebesgue integrable function is again Riemann/Lebesgue integrable. This is true if you assume some continuity somewhere, though I forget the details.

#### Damiano Testa (Apr 05 2021 at 15:00):

If I remember correctly, this plays with the fact that every subset of a set of measure zero is measurable (and has measure zero), but filtering via a further measurable function messes things up. Hopefully, someone who actually knows some analysis can provide a better explanation!

#### Kevin Buzzard (Apr 05 2021 at 15:01):

Isn't there some continuous increasing function from [0,1] to [0,1] which maps some positive measure cantor set to a zero measure cantor set and then you could have some other function which is crazy on the zero measure cantor set and then you're in trouble when you compose

#### Damiano Testa (Apr 05 2021 at 15:02):

Yes, this is also similar to what I had in mind.

#### Mario Carneiro (Apr 05 2021 at 15:02):

IIRC the lebesgue measurable functions are basically homs Borel -> Lebesgue so they only compose with Borel -> Borel which are borel measurable functions

#### Mario Carneiro (Apr 05 2021 at 15:04):

I don't think Lebesgue -> Lebesgue functions are interesting but I forget why

#### Anatole Dedecker (Apr 05 2021 at 21:01):

FYI, I have a non-PRed proof of the following :

lemma variable_change {a b : ℝ} {f φ φ' : ℝ → ℝ}
(hφ : ∀ x ∈ interval a b, has_deriv_at φ (φ' x) x)
(hφ' : continuous_on φ' (interval a b))
(hf : ∀ x ∈ φ '' (interval a b), continuous_at f x)
(hfm : ∀ x ∈ φ '' (interval a b), measurable_at_filter f (𝓝 x)) :
∫ t in a..b, f (φ t) * (φ' t) = ∫ t in (φ a)..(φ b), f t :=
sorry


I didn't have time to PR this and all the other interesting things I proved while working on Gauss Integral, but I want to get back to it soon. I will try to generalize it to any type, measure, ... but I don't know it that will actually help you

#### Benjamin Davidson (Apr 06 2021 at 16:49):

First of all, thank you everyone for all your help. I've never taken a measure theory course so I apologize that some of the discussion went over my head.

Do I understand correctly that it is notpossible to assume that f and g are interval_integrable? And, if so, is it necessary to assume that they are both continuous?

Additionally, I've opened #7065 which includes the lemma in my original post. Since I may not have the mathematical knowledge I need to do this I am welcoming any help.

#### Damiano Testa (Apr 06 2021 at 20:01):

It is not necessary that they be both continuous, it is sufficient. You can get away with one being continuous and the other one integrable, though.

#### Benjamin Davidson (Apr 07 2021 at 01:10):

@Damiano Testa Thanks! I'll give this a shot, though I have a feeling it might be beyond me.

#### Benjamin Davidson (Apr 09 2021 at 05:28):

I'm still stuck on this. I think the key is docs#measure_theory.integrable_map_measure but I haven't been able to figure it out yet. If anyone has a strategy or approach to this proof that they would be willing to share that would be a big help!

Last updated: May 10 2021 at 07:15 UTC