integrability under translation

Stream: Is there code for X?

[LiXiang]

Is there the following lemma somewhere?

variables {E : Type}
[normed_add_comm_group E] [normed_space ℂ E] [complete_space E]

lemma integrable_comp_add_left {f:ℝ → E}{a b:ℝ}
(hf : interval_integrable f measure_theory.measure_space.volume a b)
(h : ℝ) :
  interval_integrable (λ x, f (h+x)) measure_theory.measure_space.volume (-h+a) (-h+b) :=
begin
  sorry,
end

[Junyan Xu]

seems not even though we have that the integrals are equal docs#interval_integral.integral_comp_add_right ...

[LiXiang]

Yes but I want precisely the integrability, which should be more fundamental

[Junyan Xu]

Probably you can use docs#measure_theory.integrable.comp_add_right, though I've not tested.