Transfer of integrability when adding constant to function · Beginner Questions

lemma "set_integrable lborel {a..b} (f::real=>real) ==> set_integrable lborel {a-c..b-c} (λx. f (x + c))"

which should be pretty obvious by integral substitution rules, but I can't find the right lemmas somehow. Could someone help me out, please? :)

Yosuke Ito (May 20 2023 at 05:13):

I searched for some convenient lemmas, but I could not find either. :cry:
I proved it using integral_substitution.

lemma "a ≤ b ⟹ set_integrable lborel {a..b} (f::real=>real) ⟹
set_integrable lborel {a-c..b-c} (λx. f (x + c))"
proof -
  let ?g = "λx. x + c"
  assume asm: "a ≤ b" "set_integrable lborel {a..b} (f::real=>real)"
  have "set_integrable lborel {?g (a-c) .. ?g (b-c)} f" using asm by simp
  moreover have "⋀x. x ∈ {a-c..b-c} ⟹ (?g has_real_derivative 1) (at x)"
    using DERIV_shift by force
  ultimately have "set_integrable lborel {a-c..b-c} (λx. f (?g x) * 1)"
    by (rule integral_substitution, simp_all add: asm)
  thus "set_integrable lborel {a-c..b-c} (λx. f (x + c))" by simp
qed

Although I added a≤b in the assumption, it could be dropped using proof by cases.

Stream: Beginner Questions

Topic: Transfer of integrability when adding constant to function

Christian Zimmerer (May 19 2023 at 12:32):

Yosuke Ito (May 20 2023 at 05:13):

Christian Zimmerer (May 21 2023 at 10:37):