integral translation

Stream: Is there code for X?

[Patrick Massot]

Do we have the non-stupid version of the following lemma?

import measure_theory.integral.interval_integral

open topological_space
open_locale interval

variables {E : Type*} [measurable_space E] [normed_group E] [normed_space ℝ E] [borel_space E]
          [second_countable_topology E] [complete_space E]

lemma interval_integral_right_translate {f : ℝ → E} (hf : continuous f) (a b c : ℝ) :
  ∫ t in (a + c)..(b + c), f t = ∫ t in a..b, f (t + c) :=
begin
  change ∫ t in ((λ x, x +c) a)..((λ x, x + c) b), f t = ∫ t in a..b, f (t + c),
  have hg : continuous_on (λ x: ℝ, (1 : ℝ)) [a, b] := continuous_on_const,
  rw ← interval_integral.integral_comp_smul_deriv _ hg hf,
  { simp },
  { intros,
    rw ← add_zero (1 : ℝ),
    exact (has_deriv_at_id' x).add (has_deriv_at_const x c) }
end

Here non stupid means using the invariance of Lebesgue measure under translation assuming only integrability of f. I wrote the above version because I don't mind assuming continuity anyway in the sphere eversion project.

[Heather Macbeth]

Maybe docs#interval_integral.integral_comp_add_left ?

[Patrick Massot]

Seems perfect!

[Patrick Massot]

It doesn't even assume integrability (of course) :octopus: