feat(measure_theory/integral/interval_integral): interval_integrable.comp

[benjamindavidson]

---

Spawned from #7012.

My current proof of interval_integrable.comp is

lemma comp [borel_space E] {μ : measure ℝ} [locally_finite_measure μ] {a b : ℝ}
  {f : ℝ → E} {g : ℝ → ℝ} (hf : continuous f) (hg : continuous g) :
  interval_integrable (λ x, (f ∘ g) x) μ a b :=
(hf.comp hg).interval_integrable a b

I ought to be able to weaken the assumptions, but I'm not sure how to go about doing so (see Zulip). All help is more than welcome!

Once everything is figured out with that lemma I hopefully can also add some specific compositions, e.g. interval_integrable.pow.

[bryangingechen]

(The GitHub actions queue is backed up, so I canceled the build of 375aa86.)