I'm trying to prove this lemma:
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? :)
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.
awesome, thank you!
Last updated: Jan 05 2025 at 20:18 UTC