Theory HOL-Analysis.Lebesgue_Integral_Substitution
section ‹Integration by Substition for the Lebesgue Integral›
theory Lebesgue_Integral_Substitution
imports Interval_Integral
begin
lemma nn_integral_substitution_aux:
fixes f :: "real ⇒ ennreal"
assumes Mf: "f ∈ borel_measurable borel"
assumes nonnegf: "⋀x. f x ≥ 0"
assumes derivg: "⋀x. x ∈ {a..b} ⟹ (g has_real_derivative g' x) (at x)"
assumes contg': "continuous_on {a..b} g'"
assumes derivg_nonneg: "⋀x. x ∈ {a..b} ⟹ g' x ≥ 0"
assumes "a < b"
shows "(∫⇧+x. f x * indicator {g a..g b} x ∂lborel) =
(∫⇧+x. f (g x) * g' x * indicator {a..b} x ∂lborel)"
proof-
from ‹a < b› have [simp]: "a ≤ b" by simp
from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and
Mg': "set_borel_measurable borel {a..b} g'"
by (simp_all only: set_measurable_continuous_on_ivl)
from derivg have derivg': "⋀x. x ∈ {a..b} ⟹ (g has_vector_derivative g' x) (at x)"
by (simp only: has_real_derivative_iff_has_vector_derivative)
have real_ind[simp]: "⋀A x. enn2real (indicator A x) = indicator A x"
by (auto split: split_indicator)
have ennreal_ind[simp]: "⋀A x. ennreal (indicator A x) = indicator A x"
by (auto split: split_indicator)
have [simp]: "⋀x A. indicator A (g x) = indicator (g -` A) x"
by (auto split: split_indicator)
from derivg derivg_nonneg have monog: "⋀x y. a ≤ x ⟹ x ≤ y ⟹ y ≤ b ⟹ g x ≤ g y"
by (rule deriv_nonneg_imp_mono) simp_all
with monog have [simp]: "g a ≤ g b" by (auto intro: mono_onD)
show ?thesis
proof (induction rule: borel_measurable_induct[OF Mf, case_names cong set mult add sup])
case (cong f1 f2)
from cong.hyps(3) have "f1 = f2" by auto
with cong show ?case by simp
next
case (set A)
from set.hyps show ?case
proof (induction rule: borel_set_induct)
case empty
thus ?case by simp
next
case (interval c d)
{
fix u v :: real assume asm: "{u..v} ⊆ {g a..g b}" "u ≤ v"
obtain u' v' where u'v': "{a..b} ∩ g-`{u..v} = {u'..v'}" "u' ≤ v'" "g u' = u" "g v' = v"
using asm by (rule_tac continuous_interval_vimage_Int[OF contg monog, of u v]) simp_all
hence "{u'..v'} ⊆ {a..b}" "{u'..v'} ⊆ g -` {u..v}" by blast+
with u'v'(2) have "u' ∈ g -` {u..v}" "v' ∈ g -` {u..v}" by auto
from u'v'(1) have [simp]: "{a..b} ∩ g -` {u..v} ∈ sets borel" by simp
have A: "continuous_on {min u' v'..max u' v'} g'"
by (simp only: u'v' max_absorb2 min_absorb1)
(intro continuous_on_subset[OF contg'], insert u'v', auto)
have "⋀x. x ∈ {u'..v'} ⟹ (g has_real_derivative g' x) (at x within {u'..v'})"
using asm by (intro has_field_derivative_subset[OF derivg] subsetD[OF ‹{u'..v'} ⊆ {a..b}›]) auto
hence B: "⋀x. min u' v' ≤ x ⟹ x ≤ max u' v' ⟹
(g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})"
by (simp only: u'v' max_absorb2 min_absorb1)
(auto simp: has_real_derivative_iff_has_vector_derivative)
have "integrable lborel (λx. indicator ({a..b} ∩ g -` {u..v}) x *⇩R g' x)"
using set_integrable_subset borel_integrable_atLeastAtMost'[OF contg']
by (metis ‹{u'..v'} ⊆ {a..b}› eucl_ivals(5) set_integrable_def sets_lborel u'v'(1))
hence "(∫⇧+x. ennreal (g' x) * indicator ({a..b} ∩ g-` {u..v}) x ∂lborel) =
(LBINT x:{a..b} ∩ g-`{u..v}. g' x)"
unfolding set_lebesgue_integral_def
by (subst nn_integral_eq_integral[symmetric])
(auto intro!: derivg_nonneg nn_integral_cong split: split_indicator)
also from interval_integral_FTC_finite[OF A B]
have "(LBINT x:{a..b} ∩ g-`{u..v}. g' x) = v - u"
by (simp add: u'v' interval_integral_Icc ‹u ≤ v›)
finally have "(∫⇧+ x. ennreal (g' x) * indicator ({a..b} ∩ g -` {u..v}) x ∂lborel) =
ennreal (v - u)" .
} note A = this
have "(∫⇧+x. indicator {c..d} (g x) * ennreal (g' x) * indicator {a..b} x ∂lborel) =
(∫⇧+ x. ennreal (g' x) * indicator ({a..b} ∩ g -` {c..d}) x ∂lborel)"
by (intro nn_integral_cong) (simp split: split_indicator)
also have "{a..b} ∩ g-`{c..d} = {a..b} ∩ g-`{max (g a) c..min (g b) d}"
using ‹a ≤ b› ‹c ≤ d›
by (auto intro!: monog intro: order.trans)
also have "(∫⇧+ x. ennreal (g' x) * indicator ... x ∂lborel) =
(if max (g a) c ≤ min (g b) d then min (g b) d - max (g a) c else 0)"
using ‹c ≤ d› by (simp add: A)
also have "... = (∫⇧+ x. indicator ({g a..g b} ∩ {c..d}) x ∂lborel)"
by (subst nn_integral_indicator) (auto intro!: measurable_sets Mg simp:)
also have "... = (∫⇧+ x. indicator {c..d} x * indicator {g a..g b} x ∂lborel)"
by (intro nn_integral_cong) (auto split: split_indicator)
finally show ?case ..
next
case (compl A)
note ‹A ∈ sets borel›[measurable]
from emeasure_mono[of "A ∩ {g a..g b}" "{g a..g b}" lborel]
have [simp]: "emeasure lborel (A ∩ {g a..g b}) ≠ top" by (auto simp: top_unique)
have [simp]: "g -` A ∩ {a..b} ∈ sets borel"
by (rule set_borel_measurable_sets[OF Mg]) auto
have [simp]: "g -` (-A) ∩ {a..b} ∈ sets borel"
by (rule set_borel_measurable_sets[OF Mg]) auto
have "(∫⇧+x. indicator (-A) x * indicator {g a..g b} x ∂lborel) =
(∫⇧+x. indicator (-A ∩ {g a..g b}) x ∂lborel)"
by (rule nn_integral_cong) (simp split: split_indicator)
also from compl have "... = emeasure lborel ({g a..g b} - A)" using derivg_nonneg
by (simp add: vimage_Compl diff_eq Int_commute[of "-A"])
also have "{g a..g b} - A = {g a..g b} - A ∩ {g a..g b}" by blast
also have "emeasure lborel ... = g b - g a - emeasure lborel (A ∩ {g a..g b})"
using ‹A ∈ sets borel› by (subst emeasure_Diff) auto
also have "emeasure lborel (A ∩ {g a..g b}) =
∫⇧+x. indicator A x * indicator {g a..g b} x ∂lborel"
using ‹A ∈ sets borel›
by (subst nn_integral_indicator[symmetric], simp, intro nn_integral_cong)
(simp split: split_indicator)
also have "... = ∫⇧+ x. indicator (g-`A ∩ {a..b}) x * ennreal (g' x * indicator {a..b} x) ∂lborel" (is "_ = ?I")
by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator)
also have "g b - g a = (LBINT x:{a..b}. g' x)" using derivg'
unfolding set_lebesgue_integral_def
by (intro integral_FTC_atLeastAtMost[symmetric])
(auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg]
has_vector_derivative_at_within)
also have "ennreal ... = (∫⇧+ x. g' x * indicator {a..b} x ∂lborel)"
using borel_integrable_atLeastAtMost'[OF contg'] unfolding set_lebesgue_integral_def
by (subst nn_integral_eq_integral)
(simp_all add: mult.commute derivg_nonneg set_integrable_def split: split_indicator)
also have Mg'': "(λx. indicator (g -` A ∩ {a..b}) x * ennreal (g' x * indicator {a..b} x))
∈ borel_measurable borel" using Mg'
by (intro borel_measurable_times_ennreal borel_measurable_indicator)
(simp_all add: mult.commute set_borel_measurable_def)
have le: "(∫⇧+x. indicator (g-`A ∩ {a..b}) x * ennreal (g' x * indicator {a..b} x) ∂lborel) ≤
(∫⇧+x. ennreal (g' x) * indicator {a..b} x ∂lborel)"
by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg)
note integrable = borel_integrable_atLeastAtMost'[OF contg']
with le have notinf: "(∫⇧+x. indicator (g-`A ∩ {a..b}) x * ennreal (g' x * indicator {a..b} x) ∂lborel) ≠ top"
by (auto simp: real_integrable_def nn_integral_set_ennreal mult.commute top_unique set_integrable_def)
have "(∫⇧+ x. g' x * indicator {a..b} x ∂lborel) - ?I =
∫⇧+ x. ennreal (g' x * indicator {a..b} x) -
indicator (g -` A ∩ {a..b}) x * ennreal (g' x * indicator {a..b} x) ∂lborel"
apply (intro nn_integral_diff[symmetric])
apply (insert Mg', simp add: mult.commute set_borel_measurable_def) []
apply (insert Mg'', simp) []
apply (simp split: split_indicator add: derivg_nonneg)
apply (rule notinf)
apply (simp split: split_indicator add: derivg_nonneg)
done
also have "... = ∫⇧+ x. indicator (-A) (g x) * ennreal (g' x) * indicator {a..b} x ∂lborel"
by (intro nn_integral_cong) (simp split: split_indicator)
finally show ?case .
next
case (union f)
then have [simp]: "⋀i. {a..b} ∩ g -` f i ∈ sets borel"
by (subst Int_commute, intro set_borel_measurable_sets[OF Mg]) auto
have "g -` (⋃i. f i) ∩ {a..b} = (⋃i. {a..b} ∩ g -` f i)" by auto
hence "g -` (⋃i. f i) ∩ {a..b} ∈ sets borel" by (auto simp del: UN_simps)
have "(∫⇧+x. indicator (⋃i. f i) x * indicator {g a..g b} x ∂lborel) =
∫⇧+x. indicator (⋃i. {g a..g b} ∩ f i) x ∂lborel"
by (intro nn_integral_cong) (simp split: split_indicator)
also from union have "... = emeasure lborel (⋃i. {g a..g b} ∩ f i)" by simp
also from union have "... = (∑i. emeasure lborel ({g a..g b} ∩ f i))"
by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def)
also from union have "... = (∑i. ∫⇧+x. indicator ({g a..g b} ∩ f i) x ∂lborel)" by simp
also have "(λi. ∫⇧+x. indicator ({g a..g b} ∩ f i) x ∂lborel) =
(λi. ∫⇧+x. indicator (f i) x * indicator {g a..g b} x ∂lborel)"
by (intro ext nn_integral_cong) (simp split: split_indicator)
also from union.IH have "(∑i. ∫⇧+x. indicator (f i) x * indicator {g a..g b} x ∂lborel) =
(∑i. ∫⇧+ x. indicator (f i) (g x) * ennreal (g' x) * indicator {a..b} x ∂lborel)" by simp
also have "(λi. ∫⇧+ x. indicator (f i) (g x) * ennreal (g' x) * indicator {a..b} x ∂lborel) =
(λi. ∫⇧+ x. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} ∩ g -` f i) x ∂lborel)"
by (intro ext nn_integral_cong) (simp split: split_indicator)
also have "(∑i. ... i) = ∫⇧+ x. (∑i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} ∩ g -` f i) x) ∂lborel"
using Mg'
apply (intro nn_integral_suminf[symmetric])
apply (rule borel_measurable_times_ennreal, simp add: mult.commute set_borel_measurable_def)
apply (rule borel_measurable_indicator, subst sets_lborel)
apply (simp_all split: split_indicator add: derivg_nonneg)
done
also have "(λx i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} ∩ g -` f i) x) =
(λx i. ennreal (g' x * indicator {a..b} x) * indicator (g -` f i) x)"
by (intro ext) (simp split: split_indicator)
also have "(∫⇧+ x. (∑i. ennreal (g' x * indicator {a..b} x) * indicator (g -` f i) x) ∂lborel) =
∫⇧+ x. ennreal (g' x * indicator {a..b} x) * (∑i. indicator (g -` f i) x) ∂lborel"
by (intro nn_integral_cong) (auto split: split_indicator simp: derivg_nonneg)
also from union have "(λx. ∑i. indicator (g -` f i) x :: ennreal) = (λx. indicator (⋃i. g -` f i) x)"
by (intro ext suminf_indicator) (auto simp: disjoint_family_on_def)
also have "(∫⇧+x. ennreal (g' x * indicator {a..b} x) * ... x ∂lborel) =
(∫⇧+x. indicator (⋃i. f i) (g x) * ennreal (g' x) * indicator {a..b} x ∂lborel)"
by (intro nn_integral_cong) (simp split: split_indicator)
finally show ?case .
qed
next
case (mult f c)
note Mf[measurable] = ‹f ∈ borel_measurable borel›
let ?I = "indicator {a..b}"
have "(λx. f (g x * ?I x) * ennreal (g' x * ?I x)) ∈ borel_measurable borel" using Mg Mg'
by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
(simp_all add: mult.commute set_borel_measurable_def)
also have "(λx. f (g x * ?I x) * ennreal (g' x * ?I x)) = (λx. f (g x) * ennreal (g' x) * ?I x)"
by (intro ext) (simp split: split_indicator)
finally have Mf': "(λx. f (g x) * ennreal (g' x) * ?I x) ∈ borel_measurable borel" .
with mult show ?case
by (subst (1 2 3) mult_ac, subst (1 2) nn_integral_cmult) (simp_all add: mult_ac)
next
case (add f2 f1)
let ?I = "indicator {a..b}"
{
fix f :: "real ⇒ ennreal" assume Mf: "f ∈ borel_measurable borel"
have "(λx. f (g x * ?I x) * ennreal (g' x * ?I x)) ∈ borel_measurable borel" using Mg Mg'
by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
(simp_all add: mult.commute set_borel_measurable_def)
also have "(λx. f (g x * ?I x) * ennreal (g' x * ?I x)) = (λx. f (g x) * ennreal (g' x) * ?I x)"
by (intro ext) (simp split: split_indicator)
finally have "(λx. f (g x) * ennreal (g' x) * ?I x) ∈ borel_measurable borel" .
} note Mf' = this[OF ‹f1 ∈ borel_measurable borel›] this[OF ‹f2 ∈ borel_measurable borel›]
have "(∫⇧+ x. (f1 x + f2 x) * indicator {g a..g b} x ∂lborel) =
(∫⇧+ x. f1 x * indicator {g a..g b} x + f2 x * indicator {g a..g b} x ∂lborel)"
by (intro nn_integral_cong) (simp split: split_indicator)
also from add have "... = (∫⇧+ x. f1 (g x) * ennreal (g' x) * indicator {a..b} x ∂lborel) +
(∫⇧+ x. f2 (g x) * ennreal (g' x) * indicator {a..b} x ∂lborel)"
by (simp_all add: nn_integral_add)
also from add have "... = (∫⇧+ x. f1 (g x) * ennreal (g' x) * indicator {a..b} x +
f2 (g x) * ennreal (g' x) * indicator {a..b} x ∂lborel)"
by (intro nn_integral_add[symmetric])
(auto simp add: Mf' derivg_nonneg split: split_indicator)
also have "... = ∫⇧+ x. (f1 (g x) + f2 (g x)) * ennreal (g' x) * indicator {a..b} x ∂lborel"
by (intro nn_integral_cong) (simp split: split_indicator add: distrib_right)
finally show ?case .
next
case (sup F)
{
fix i
let ?I = "indicator {a..b}"
have "(λx. F i (g x * ?I x) * ennreal (g' x * ?I x)) ∈ borel_measurable borel" using Mg Mg'
by (rule_tac borel_measurable_times_ennreal, rule_tac measurable_compose[OF _ sup.hyps(1)])
(simp_all add: mult.commute set_borel_measurable_def)
also have "(λx. F i (g x * ?I x) * ennreal (g' x * ?I x)) = (λx. F i (g x) * ennreal (g' x) * ?I x)"
by (intro ext) (simp split: split_indicator)
finally have "... ∈ borel_measurable borel" .
} note Mf' = this
have "(∫⇧+x. (SUP i. F i x) * indicator {g a..g b} x ∂lborel) =
∫⇧+x. (SUP i. F i x* indicator {g a..g b} x) ∂lborel"
by (intro nn_integral_cong) (simp split: split_indicator)
also from sup have "... = (SUP i. ∫⇧+x. F i x* indicator {g a..g b} x ∂lborel)"
by (intro nn_integral_monotone_convergence_SUP)
(auto simp: incseq_def le_fun_def split: split_indicator)
also from sup have "... = (SUP i. ∫⇧+x. F i (g x) * ennreal (g' x) * indicator {a..b} x ∂lborel)"
by simp
also from sup have "... = ∫⇧+x. (SUP i. F i (g x) * ennreal (g' x) * indicator {a..b} x) ∂lborel"
by (intro nn_integral_monotone_convergence_SUP[symmetric])
(auto simp: incseq_def le_fun_def derivg_nonneg Mf' split: split_indicator
intro!: mult_right_mono)
also from sup have "... = ∫⇧+x. (SUP i. F i (g x)) * ennreal (g' x) * indicator {a..b} x ∂lborel"
by (subst mult.assoc, subst mult.commute, subst SUP_mult_left_ennreal)
(auto split: split_indicator simp: derivg_nonneg mult_ac)
finally show ?case by (simp add: image_comp)
qed
qed
theorem nn_integral_substitution:
fixes f :: "real ⇒ real"
assumes Mf[measurable]: "set_borel_measurable borel {g a..g b} f"
assumes derivg: "⋀x. x ∈ {a..b} ⟹ (g has_real_derivative g' x) (at x)"
assumes contg': "continuous_on {a..b} g'"
assumes derivg_nonneg: "⋀x. x ∈ {a..b} ⟹ g' x ≥ 0"
assumes "a ≤ b"
shows "(∫⇧+x. f x * indicator {g a..g b} x ∂lborel) =
(∫⇧+x. f (g x) * g' x * indicator {a..b} x ∂lborel)"
proof (cases "a = b")
assume "a ≠ b"
with ‹a ≤ b› have "a < b" by auto
let ?f' = "λx. f x * indicator {g a..g b} x"
from derivg derivg_nonneg have monog: "⋀x y. a ≤ x ⟹ x ≤ y ⟹ y ≤ b ⟹ g x ≤ g y"
by (rule deriv_nonneg_imp_mono) simp_all
have bounds: "⋀x. x ≥ a ⟹ x ≤ b ⟹ g x ≥ g a" "⋀x. x ≥ a ⟹ x ≤ b ⟹ g x ≤ g b"
by (auto intro: monog)
from derivg_nonneg have nonneg:
"⋀f x. x ≥ a ⟹ x ≤ b ⟹ g' x ≠ 0 ⟹ f x * ennreal (g' x) ≥ 0 ⟹ f x ≥ 0"
by (force simp: field_simps)
have nonneg': "⋀x. a ≤ x ⟹ x ≤ b ⟹ ¬ 0 ≤ f (g x) ⟹ 0 ≤ f (g x) * g' x ⟹ g' x = 0"
by (metis atLeastAtMost_iff derivg_nonneg eq_iff mult_eq_0_iff mult_le_0_iff)
have "(∫⇧+x. f x * indicator {g a..g b} x ∂lborel) =
(∫⇧+x. ennreal (?f' x) * indicator {g a..g b} x ∂lborel)"
by (intro nn_integral_cong)
(auto split: split_indicator split_max simp: zero_ennreal.rep_eq ennreal_neg)
also have "... = ∫⇧+ x. ?f' (g x) * ennreal (g' x) * indicator {a..b} x ∂lborel" using Mf
by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg ‹a < b›])
(auto simp add: mult.commute set_borel_measurable_def)
also have "... = ∫⇧+ x. f (g x) * ennreal (g' x) * indicator {a..b} x ∂lborel"
by (intro nn_integral_cong) (auto split: split_indicator simp: max_def dest: bounds)
also have "... = ∫⇧+x. ennreal (f (g x) * g' x * indicator {a..b} x) ∂lborel"
by (intro nn_integral_cong) (auto simp: mult.commute derivg_nonneg ennreal_mult' split: split_indicator)
finally show ?thesis .
qed auto
theorem integral_substitution:
assumes integrable: "set_integrable lborel {g a..g b} f"
assumes derivg: "⋀x. x ∈ {a..b} ⟹ (g has_real_derivative g' x) (at x)"
assumes contg': "continuous_on {a..b} g'"
assumes derivg_nonneg: "⋀x. x ∈ {a..b} ⟹ g' x ≥ 0"
assumes "a ≤ b"
shows "set_integrable lborel {a..b} (λx. f (g x) * g' x)"
and "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)"
proof-
from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
with contg' have Mg: "set_borel_measurable borel {a..b} g"
and Mg': "set_borel_measurable borel {a..b} g'"
by (simp_all only: set_measurable_continuous_on_ivl)
from derivg derivg_nonneg have monog: "⋀x y. a ≤ x ⟹ x ≤ y ⟹ y ≤ b ⟹ g x ≤ g y"
by (rule deriv_nonneg_imp_mono) simp_all
have "(λx. ennreal (f x) * indicator {g a..g b} x) =
(λx. ennreal (f x * indicator {g a..g b} x))"
by (intro ext) (simp split: split_indicator)
with integrable have M1: "(λx. f x * indicator {g a..g b} x) ∈ borel_measurable borel"
by (force simp: mult.commute set_integrable_def)
from integrable have M2: "(λx. -f x * indicator {g a..g b} x) ∈ borel_measurable borel"
by (force simp: mult.commute set_integrable_def)
have "(LBINT x. (f x :: real) * indicator {g a..g b} x) =
enn2real (∫⇧+ x. ennreal (f x) * indicator {g a..g b} x ∂lborel) -
enn2real (∫⇧+ x. ennreal (- (f x)) * indicator {g a..g b} x ∂lborel)" using integrable
unfolding set_integrable_def
by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ennreal mult.commute)
also have *: "(∫⇧+x. ennreal (f x) * indicator {g a..g b} x ∂lborel) =
(∫⇧+x. ennreal (f x * indicator {g a..g b} x) ∂lborel)"
by (intro nn_integral_cong) (simp split: split_indicator)
also from M1 * have A: "(∫⇧+ x. ennreal (f x * indicator {g a..g b} x) ∂lborel) =
(∫⇧+ x. ennreal (f (g x) * g' x * indicator {a..b} x) ∂lborel)"
by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg ‹a ≤ b›])
(auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)
also have **: "(∫⇧+ x. ennreal (- (f x)) * indicator {g a..g b} x ∂lborel) =
(∫⇧+ x. ennreal (- (f x) * indicator {g a..g b} x) ∂lborel)"
by (intro nn_integral_cong) (simp split: split_indicator)
also from M2 ** have B: "(∫⇧+ x. ennreal (- (f x) * indicator {g a..g b} x) ∂lborel) =
(∫⇧+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) ∂lborel)"
by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg ‹a ≤ b›])
(auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)
also {
from integrable have Mf: "set_borel_measurable borel {g a..g b} f"
unfolding set_borel_measurable_def set_integrable_def by simp
from measurable_compose Mg Mf Mg' borel_measurable_times
have "(λx. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
(g' x * indicator {a..b} x)) ∈ borel_measurable borel" (is "?f ∈ _")
by (simp add: mult.commute set_borel_measurable_def)
also have "?f = (λx. f (g x) * g' x * indicator {a..b} x)"
using monog by (intro ext) (auto split: split_indicator)
finally show "set_integrable lborel {a..b} (λx. f (g x) * g' x)"
using A B integrable unfolding real_integrable_def set_integrable_def
by (simp_all add: nn_integral_set_ennreal mult.commute)
} note integrable' = this
have "enn2real (∫⇧+ x. ennreal (f (g x) * g' x * indicator {a..b} x) ∂lborel) -
enn2real (∫⇧+ x. ennreal (-f (g x) * g' x * indicator {a..b} x) ∂lborel) =
(LBINT x. f (g x) * g' x * indicator {a..b} x)"
using integrable' unfolding set_integrable_def
by (subst real_lebesgue_integral_def) (simp_all add: field_simps)
finally show "(LBINT x. f x * indicator {g a..g b} x) =
(LBINT x. f (g x) * g' x * indicator {a..b} x)" .
qed
theorem interval_integral_substitution:
assumes integrable: "set_integrable lborel {g a..g b} f"
assumes derivg: "⋀x. x ∈ {a..b} ⟹ (g has_real_derivative g' x) (at x)"
assumes contg': "continuous_on {a..b} g'"
assumes derivg_nonneg: "⋀x. x ∈ {a..b} ⟹ g' x ≥ 0"
assumes "a ≤ b"
shows "set_integrable lborel {a..b} (λx. f (g x) * g' x)"
and "(LBINT x=g a..g b. f x) = (LBINT x=a..b. f (g x) * g' x)"
apply (rule integral_substitution[OF assms], simp, simp)
apply (subst (1 2) interval_integral_Icc, fact)
apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact)
using integral_substitution(2)[OF assms]
apply (simp add: mult.commute set_lebesgue_integral_def)
done
lemma set_borel_integrable_singleton[simp]: "set_integrable lborel {x} (f :: real ⇒ real)"
unfolding set_integrable_def
by (subst integrable_discrete_difference[where X="{x}" and g="λ_. 0"]) auto
end