interval_integrable.comp

Stream: maths

[Benjamin Davidson]

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]

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

[Damiano Testa]

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]

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]

or integration on a preimage measure

[Mario Carneiro]

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

[Mario Carneiro]

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

[Benjamin Davidson]

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]

Those two should be basically the same thing

[Benjamin Davidson]

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]

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

[Damiano Testa]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Riccardo Brasca]

https://mathoverflow.net/questions/31603/why-do-probabilists-take-random-variables-to-be-borel-and-not-lebesgue-measura is probably relevant

[Anatole Dedecker]

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]

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]

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]

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

[Benjamin Davidson]

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!