src/HOL/Probability/Lebesgue_Integral_Substitution.thy
author hoelzl
Thu Jan 22 14:51:08 2015 +0100 (2015-01-22)
changeset 59425 c5e79df8cc21
parent 59092 d469103c0737
child 59452 2538b2c51769
permissions -rw-r--r--
import general thms from Density_Compiler
     1 (*  Title:      HOL/Probability/Lebesgue_Integral_Substitution.thy
     2     Author:     Manuel Eberl
     3 
     4     Provides lemmas for integration by substitution for the basic integral types.
     5     Note that the substitution function must have a nonnegative derivative.
     6     This could probably be weakened somehow.
     7 *)
     8 
     9 section {* Integration by Substition *}
    10 
    11 theory Lebesgue_Integral_Substitution
    12 imports Interval_Integral
    13 begin
    14 
    15 lemma measurable_sets_borel:
    16     "\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel"
    17   by (drule (1) measurable_sets) simp
    18 
    19 lemma closure_Iii: 
    20   assumes "a < b"
    21   shows "closure {a<..<b::real} = {a..b}"
    22 proof-
    23   have "{a<..<b} = ball ((a+b)/2) ((b-a)/2)" by (auto simp: dist_real_def field_simps not_less)
    24   also from assms have "closure ... = cball ((a+b)/2) ((b-a)/2)" by (intro closure_ball) simp
    25   also have "... = {a..b}" by (auto simp: dist_real_def field_simps not_less)
    26   finally show ?thesis .
    27 qed
    28 
    29 lemma continuous_ge_on_Iii:
    30   assumes "continuous_on {c..d} g" "\<And>x. x \<in> {c<..<d} \<Longrightarrow> g x \<ge> a" "c < d" "x \<in> {c..d}"
    31   shows "g (x::real) \<ge> (a::real)"
    32 proof-
    33   from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_Iii[symmetric])
    34   also from assms(2) have "{c<..<d} \<subseteq> (g -` {a..} \<inter> {c..d})" by auto
    35   hence "closure {c<..<d} \<subseteq> closure (g -` {a..} \<inter> {c..d})" by (rule closure_mono)
    36   also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
    37     by (auto simp: continuous_on_closed_vimage)
    38   hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
    39   finally show ?thesis using `x \<in> {c..d}` by auto 
    40 qed 
    41 
    42 lemma interior_real_semiline':
    43   fixes a :: real
    44   shows "interior {..a} = {..<a}"
    45 proof -
    46   {
    47     fix y
    48     assume "a > y"
    49     then have "y \<in> interior {..a}"
    50       apply (simp add: mem_interior)
    51       apply (rule_tac x="(a-y)" in exI)
    52       apply (auto simp add: dist_norm)
    53       done
    54   }
    55   moreover
    56   {
    57     fix y
    58     assume "y \<in> interior {..a}"
    59     then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}"
    60       using mem_interior_cball[of y "{..a}"] by auto
    61     moreover from e have "y + e \<in> cball y e"
    62       by (auto simp add: cball_def dist_norm)
    63     ultimately have "a \<ge> y + e" by auto
    64     then have "a > y" using e by auto
    65   }
    66   ultimately show ?thesis by auto
    67 qed
    68 
    69 lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
    70 proof-
    71   have "{a..b} = {a..} \<inter> {..b}" by auto
    72   also have "interior ... = {a<..} \<inter> {..<b}" 
    73     by (simp add: interior_real_semiline interior_real_semiline')
    74   also have "... = {a<..<b}" by auto
    75   finally show ?thesis .
    76 qed
    77 
    78 lemma nn_integral_indicator_singleton[simp]:
    79   assumes [measurable]: "{y} \<in> sets M"
    80   shows "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = max 0 (f y) * emeasure M {y}"
    81 proof-
    82   have "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = (\<integral>\<^sup>+x. max 0 (f y) * indicator {y} x \<partial>M)"
    83     by (subst nn_integral_max_0[symmetric]) (auto intro!: nn_integral_cong split: split_indicator)
    84   then show ?thesis
    85     by (simp add: nn_integral_cmult)
    86 qed
    87 
    88 lemma nn_integral_set_ereal:
    89   "(\<integral>\<^sup>+x. ereal (f x) * indicator A x \<partial>M) = (\<integral>\<^sup>+x. ereal (f x * indicator A x) \<partial>M)"
    90   by (rule nn_integral_cong) (simp split: split_indicator)
    91 
    92 lemma nn_integral_indicator_singleton'[simp]:
    93   assumes [measurable]: "{y} \<in> sets M"
    94   shows "(\<integral>\<^sup>+x. ereal (f x * indicator {y} x) \<partial>M) = max 0 (f y) * emeasure M {y}"
    95   by (subst nn_integral_set_ereal[symmetric]) simp
    96 
    97 lemma set_borel_measurable_sets:
    98   fixes f :: "_ \<Rightarrow> _::real_normed_vector"
    99   assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
   100   shows "f -` B \<inter> X \<in> sets M"
   101 proof -
   102   have "f \<in> borel_measurable (restrict_space M X)"
   103     using assms by (subst borel_measurable_restrict_space_iff) auto
   104   then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
   105     by (rule measurable_sets) fact
   106   with `X \<in> sets M` show ?thesis
   107     by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
   108 qed
   109 
   110 lemma borel_set_induct[consumes 1, case_names empty interval compl union]:
   111   assumes "A \<in> sets borel" 
   112   assumes empty: "P {}" and int: "\<And>a b. a \<le> b \<Longrightarrow> P {a..b}" and compl: "\<And>A. A \<in> sets borel \<Longrightarrow> P A \<Longrightarrow> P (-A)" and
   113           un: "\<And>f. disjoint_family f \<Longrightarrow> (\<And>i. f i \<in> sets borel) \<Longrightarrow>  (\<And>i. P (f i)) \<Longrightarrow> P (\<Union>i::nat. f i)"
   114   shows "P (A::real set)"
   115 proof-
   116   let ?G = "range (\<lambda>(a,b). {a..b::real})"
   117   have "Int_stable ?G" "?G \<subseteq> Pow UNIV" "A \<in> sigma_sets UNIV ?G" 
   118       using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def)
   119   thus ?thesis
   120   proof (induction rule: sigma_sets_induct_disjoint) 
   121     case (union f)
   122       from union.hyps(2) have "\<And>i. f i \<in> sets borel" by (auto simp: borel_eq_atLeastAtMost)
   123       with union show ?case by (auto intro: un)
   124   next
   125     case (basic A)
   126     then obtain a b where "A = {a .. b}" by auto
   127     then show ?case
   128       by (cases "a \<le> b") (auto intro: int empty)
   129   qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost)
   130 qed
   131 
   132 definition "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s"
   133 
   134 lemma mono_onI:
   135   "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r \<le> s \<Longrightarrow> f r \<le> f s) \<Longrightarrow> mono_on f A"
   136   unfolding mono_on_def by simp
   137 
   138 lemma mono_onD:
   139   "\<lbrakk>mono_on f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
   140   unfolding mono_on_def by simp
   141 
   142 lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on f A"
   143   unfolding mono_def mono_on_def by auto
   144 
   145 lemma mono_on_subset: "mono_on f A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on f B"
   146   unfolding mono_on_def by auto
   147 
   148 definition "strict_mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s"
   149 
   150 lemma strict_mono_onI:
   151   "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on f A"
   152   unfolding strict_mono_on_def by simp
   153 
   154 lemma strict_mono_onD:
   155   "\<lbrakk>strict_mono_on f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
   156   unfolding strict_mono_on_def by simp
   157 
   158 lemma mono_on_greaterD:
   159   assumes "mono_on g A" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)"
   160   shows "x > y"
   161 proof (rule ccontr)
   162   assume "\<not>x > y"
   163   hence "x \<le> y" by (simp add: not_less)
   164   from assms(1-3) and this have "g x \<le> g y" by (rule mono_onD)
   165   with assms(4) show False by simp
   166 qed
   167 
   168 lemma strict_mono_inv:
   169   fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)"
   170   assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x"
   171   shows "strict_mono g"
   172 proof
   173   fix x y :: 'b assume "x < y"
   174   from `surj f` obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast
   175   with `x < y` and `strict_mono f` have "x' < y'" by (simp add: strict_mono_less)
   176   with inv show "g x < g y" by simp
   177 qed
   178 
   179 lemma strict_mono_on_imp_inj_on:
   180   assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder)) A"
   181   shows "inj_on f A"
   182 proof (rule inj_onI)
   183   fix x y assume "x \<in> A" "y \<in> A" "f x = f y"
   184   thus "x = y"
   185     by (cases x y rule: linorder_cases)
   186        (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) 
   187 qed
   188 
   189 lemma strict_mono_on_leD:
   190   assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y"
   191   shows "f x \<le> f y"
   192 proof (insert le_less_linear[of y x], elim disjE)
   193   assume "x < y"
   194   with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all
   195   thus ?thesis by (rule less_imp_le)
   196 qed (insert assms, simp)
   197 
   198 lemma strict_mono_on_eqD:
   199   fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)"
   200   assumes "strict_mono_on f A" "f x = f y" "x \<in> A" "y \<in> A"
   201   shows "y = x"
   202   using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD)
   203 
   204 lemma mono_on_imp_deriv_nonneg:
   205   assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)"
   206   assumes "x \<in> interior A"
   207   shows "D \<ge> 0"
   208 proof (rule tendsto_le_const)
   209   let ?A' = "(\<lambda>y. y - x) ` interior A"
   210   from deriv show "((\<lambda>h. (f (x + h) - f x) / h) ---> D) (at 0)"
   211       by (simp add: field_has_derivative_at has_field_derivative_def)
   212   from mono have mono': "mono_on f (interior A)" by (rule mono_on_subset) (rule interior_subset)
   213 
   214   show "eventually (\<lambda>h. (f (x + h) - f x) / h \<ge> 0) (at 0)"
   215   proof (subst eventually_at_topological, intro exI conjI ballI impI)
   216     have "open (interior A)" by simp
   217     hence "open (op + (-x) ` interior A)" by (rule open_translation)
   218     also have "(op + (-x) ` interior A) = ?A'" by auto
   219     finally show "open ?A'" .
   220   next
   221     from `x \<in> interior A` show "0 \<in> ?A'" by auto
   222   next
   223     fix h assume "h \<in> ?A'"
   224     hence "x + h \<in> interior A" by auto
   225     with mono' and `x \<in> interior A` show "(f (x + h) - f x) / h \<ge> 0"
   226       by (cases h rule: linorder_cases[of _ 0])
   227          (simp_all add: divide_nonpos_neg divide_nonneg_pos mono_onD field_simps)
   228   qed
   229 qed simp
   230 
   231 lemma strict_mono_on_imp_mono_on: 
   232   "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A \<Longrightarrow> mono_on f A"
   233   by (rule mono_onI, rule strict_mono_on_leD)
   234 
   235 lemma has_real_derivative_imp_continuous_on:
   236   assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
   237   shows "continuous_on A f"
   238   apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def)
   239   apply (intro ballI Deriv.differentiableI)
   240   apply (rule has_field_derivative_subset[OF assms])
   241   apply simp_all
   242   done
   243 
   244 lemma closure_contains_Sup:
   245   fixes S :: "real set"
   246   assumes "S \<noteq> {}" "bdd_above S"
   247   shows "Sup S \<in> closure S"
   248 proof-
   249   have "Inf (uminus ` S) \<in> closure (uminus ` S)" 
   250       using assms by (intro closure_contains_Inf) auto
   251   also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def)
   252   also have "closure (uminus ` S) = uminus ` closure S"
   253       by (rule sym, intro closure_injective_linear_image) (auto intro: linearI)
   254   finally show ?thesis by auto
   255 qed
   256 
   257 lemma closed_contains_Sup:
   258   fixes S :: "real set"
   259   shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
   260   by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
   261 
   262 lemma deriv_nonneg_imp_mono:
   263   assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   264   assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   265   assumes ab: "a \<le> b"
   266   shows "g a \<le> g b"
   267 proof (cases "a < b")
   268   assume "a < b"
   269   from deriv have "\<forall>x. x \<ge> a \<and> x \<le> b \<longrightarrow> (g has_real_derivative g' x) (at x)" by simp
   270   from MVT2[OF `a < b` this] and deriv 
   271     obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast
   272   from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp
   273   with g_ab show ?thesis by simp
   274 qed (insert ab, simp)
   275 
   276 lemma continuous_interval_vimage_Int:
   277   assumes "continuous_on {a::real..b} g" and mono: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
   278   assumes "a \<le> b" "(c::real) \<le> d" "{c..d} \<subseteq> {g a..g b}"
   279   obtains c' d' where "{a..b} \<inter> g -` {c..d} = {c'..d'}" "c' \<le> d'" "g c' = c" "g d' = d"
   280 proof-
   281     let ?A = "{a..b} \<inter> g -` {c..d}"
   282     from IVT'[of g a c b, OF _ _ `a \<le> b` assms(1)] assms(4,5) 
   283          obtain c'' where c'': "c'' \<in> ?A" "g c'' = c" by auto
   284     from IVT'[of g a d b, OF _ _ `a \<le> b` assms(1)] assms(4,5) 
   285          obtain d'' where d'': "d'' \<in> ?A" "g d'' = d" by auto
   286     hence [simp]: "?A \<noteq> {}" by blast
   287 
   288     def c' \<equiv> "Inf ?A" and d' \<equiv> "Sup ?A"
   289     have "?A \<subseteq> {c'..d'}" unfolding c'_def d'_def
   290         by (intro subsetI) (auto intro: cInf_lower cSup_upper)
   291     moreover from assms have "closed ?A" 
   292         using continuous_on_closed_vimage[of "{a..b}" g] by (subst Int_commute) simp
   293     hence c'd'_in_set: "c' \<in> ?A" "d' \<in> ?A" unfolding c'_def d'_def
   294         by ((intro closed_contains_Inf closed_contains_Sup, simp_all)[])+
   295     hence "{c'..d'} \<subseteq> ?A" using assms 
   296         by (intro subsetI)
   297            (auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x] 
   298                  intro!: mono)
   299     moreover have "c' \<le> d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto
   300     moreover have "g c' \<le> c" "g d' \<ge> d"
   301       apply (insert c'' d'' c'd'_in_set)
   302       apply (subst c''(2)[symmetric])
   303       apply (auto simp: c'_def intro!: mono cInf_lower c'') []
   304       apply (subst d''(2)[symmetric])
   305       apply (auto simp: d'_def intro!: mono cSup_upper d'') []
   306       done
   307     with c'd'_in_set have "g c' = c" "g d' = d" by auto
   308     ultimately show ?thesis using that by blast
   309 qed
   310 
   311 lemma nn_integral_substitution_aux:
   312   fixes f :: "real \<Rightarrow> ereal"
   313   assumes Mf: "f \<in> borel_measurable borel"
   314   assumes nonnegf: "\<And>x. f x \<ge> 0"
   315   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   316   assumes contg': "continuous_on {a..b} g'" 
   317   assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   318   assumes "a < b"
   319   shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
   320              (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
   321 proof-
   322   from `a < b` have [simp]: "a \<le> b" by simp
   323   from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
   324   from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and 
   325                              Mg': "set_borel_measurable borel {a..b} g'" 
   326       by (simp_all only: set_measurable_continuous_on_ivl)
   327   from derivg have derivg': "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
   328     by (simp only: has_field_derivative_iff_has_vector_derivative)
   329 
   330   have real_ind[simp]: "\<And>A x. real (indicator A x :: ereal) = indicator A x" 
   331       by (auto split: split_indicator)
   332   have ereal_ind[simp]: "\<And>A x. ereal (indicator A x) = indicator A x" 
   333       by (auto split: split_indicator)
   334   have [simp]: "\<And>x A. indicator A (g x) = indicator (g -` A) x" 
   335       by (auto split: split_indicator)
   336 
   337   from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
   338     by (rule deriv_nonneg_imp_mono) simp_all
   339   with monog have [simp]: "g a \<le> g b" by (auto intro: mono_onD)
   340 
   341   show ?thesis
   342   proof (induction rule: borel_measurable_induct[OF Mf nonnegf, case_names cong set mult add sup])
   343     case (cong f1 f2)
   344     from cong.hyps(3) have "f1 = f2" by auto
   345     with cong show ?case by simp
   346   next
   347     case (set A)
   348     from set.hyps show ?case
   349     proof (induction rule: borel_set_induct)
   350       case empty
   351       thus ?case by simp
   352     next
   353       case (interval c d)
   354       {
   355         fix u v :: real assume asm: "{u..v} \<subseteq> {g a..g b}" "u \<le> v"
   356         
   357         obtain u' v' where u'v': "{a..b} \<inter> g-`{u..v} = {u'..v'}" "u' \<le> v'" "g u' = u" "g v' = v"
   358              using asm by (rule_tac continuous_interval_vimage_Int[OF contg monog, of u v]) simp_all
   359         hence "{u'..v'} \<subseteq> {a..b}" "{u'..v'} \<subseteq> g -` {u..v}" by blast+
   360         with u'v'(2) have "u' \<in> g -` {u..v}" "v' \<in> g -` {u..v}" by auto
   361         from u'v'(1) have [simp]: "{a..b} \<inter> g -` {u..v} \<in> sets borel" by simp
   362         
   363         have A: "continuous_on {min u' v'..max u' v'} g'"
   364             by (simp only: u'v' max_absorb2 min_absorb1) 
   365                (intro continuous_on_subset[OF contg'], insert u'v', auto)
   366         have "\<And>x. x \<in> {u'..v'} \<Longrightarrow> (g has_real_derivative g' x) (at x within {u'..v'})"
   367            using asm by (intro has_field_derivative_subset[OF derivg] set_mp[OF `{u'..v'} \<subseteq> {a..b}`]) auto
   368         hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow> 
   369                       (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})" 
   370             by (simp only: u'v' max_absorb2 min_absorb1) 
   371                (auto simp: has_field_derivative_iff_has_vector_derivative)
   372         have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
   373           by (rule set_integrable_subset[OF borel_integrable_atLeastAtMost'[OF contg']]) simp_all
   374         hence "(\<integral>\<^sup>+x. ereal (g' x) * indicator ({a..b} \<inter> g-` {u..v}) x \<partial>lborel) = 
   375                    LBINT x:{a..b} \<inter> g-`{u..v}. g' x" 
   376           by (subst ereal_ind[symmetric], subst times_ereal.simps, subst nn_integral_eq_integral)
   377              (auto intro: measurable_sets Mg simp: derivg_nonneg mult.commute split: split_indicator)
   378         also from interval_integral_FTC_finite[OF A B]
   379             have "LBINT x:{a..b} \<inter> g-`{u..v}. g' x = v - u"
   380                 by (simp add: u'v' interval_integral_Icc `u \<le> v`)
   381         finally have "(\<integral>\<^sup>+ x. ereal (g' x) * indicator ({a..b} \<inter> g -` {u..v}) x \<partial>lborel) =
   382                            ereal (v - u)" .
   383       } note A = this
   384   
   385       have "(\<integral>\<^sup>+x. indicator {c..d} (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) =
   386                (\<integral>\<^sup>+ x. ereal (g' x) * indicator ({a..b} \<inter> g -` {c..d}) x \<partial>lborel)" 
   387         by (intro nn_integral_cong) (simp split: split_indicator)
   388       also have "{a..b} \<inter> g-`{c..d} = {a..b} \<inter> g-`{max (g a) c..min (g b) d}" 
   389         using `a \<le> b` `c \<le> d`
   390         by (auto intro!: monog intro: order.trans)
   391       also have "(\<integral>\<^sup>+ x. ereal (g' x) * indicator ... x \<partial>lborel) =
   392         (if max (g a) c \<le> min (g b) d then min (g b) d - max (g a) c else 0)"
   393          using `c \<le> d` by (simp add: A)
   394       also have "... = (\<integral>\<^sup>+ x. indicator ({g a..g b} \<inter> {c..d}) x \<partial>lborel)"
   395         by (subst nn_integral_indicator) (auto intro!: measurable_sets Mg simp:)
   396       also have "... = (\<integral>\<^sup>+ x. indicator {c..d} x * indicator {g a..g b} x \<partial>lborel)"
   397         by (intro nn_integral_cong) (auto split: split_indicator)
   398       finally show ?case ..
   399 
   400       next
   401 
   402       case (compl A)
   403       note `A \<in> sets borel`[measurable]
   404       from emeasure_mono[of "A \<inter> {g a..g b}" "{g a..g b}" lborel]
   405           have [simp]: "emeasure lborel (A \<inter> {g a..g b}) \<noteq> \<infinity>" by auto
   406       have [simp]: "g -` A \<inter> {a..b} \<in> sets borel"
   407         by (rule set_borel_measurable_sets[OF Mg]) auto
   408       have [simp]: "g -` (-A) \<inter> {a..b} \<in> sets borel"
   409         by (rule set_borel_measurable_sets[OF Mg]) auto
   410 
   411       have "(\<integral>\<^sup>+x. indicator (-A) x * indicator {g a..g b} x \<partial>lborel) = 
   412                 (\<integral>\<^sup>+x. indicator (-A \<inter> {g a..g b}) x \<partial>lborel)" 
   413         by (rule nn_integral_cong) (simp split: split_indicator)
   414       also from compl have "... = emeasure lborel ({g a..g b} - A)" using derivg_nonneg
   415         by (simp add: vimage_Compl diff_eq Int_commute[of "-A"])
   416       also have "{g a..g b} - A = {g a..g b} - A \<inter> {g a..g b}" by blast
   417       also have "emeasure lborel ... = g b - g a - emeasure lborel (A \<inter> {g a..g b})"
   418              using `A \<in> sets borel` by (subst emeasure_Diff) (auto simp: real_of_ereal_minus)
   419      also have "emeasure lborel (A \<inter> {g a..g b}) = 
   420                     \<integral>\<^sup>+x. indicator A x * indicator {g a..g b} x \<partial>lborel" 
   421        using `A \<in> sets borel`
   422        by (subst nn_integral_indicator[symmetric], simp, intro nn_integral_cong)
   423           (simp split: split_indicator)
   424       also have "... = \<integral>\<^sup>+ x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel" (is "_ = ?I")
   425         by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator)
   426       also have "g b - g a = LBINT x:{a..b}. g' x" using derivg'
   427         by (intro integral_FTC_atLeastAtMost[symmetric])
   428            (auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg]
   429                  has_vector_derivative_at_within)
   430       also have "ereal ... = \<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel"
   431         using borel_integrable_atLeastAtMost'[OF contg']
   432         by (subst nn_integral_eq_integral)
   433            (simp_all add: mult.commute derivg_nonneg split: split_indicator)
   434       also have Mg'': "(\<lambda>x. indicator (g -` A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x))
   435                             \<in> borel_measurable borel" using Mg'
   436         by (intro borel_measurable_ereal_times borel_measurable_indicator)
   437            (simp_all add: mult.commute)
   438       have le: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel) \<le>
   439                         (\<integral>\<^sup>+x. ereal (g' x) * indicator {a..b} x \<partial>lborel)"
   440          by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg)
   441       note integrable = borel_integrable_atLeastAtMost'[OF contg']
   442       with le have notinf: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel) \<noteq> \<infinity>"
   443           by (auto simp: real_integrable_def nn_integral_set_ereal mult.commute)
   444       have "(\<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel) - ?I = 
   445                   \<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) - 
   446                         indicator (g -` A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel"
   447         apply (intro nn_integral_diff[symmetric])
   448         apply (insert Mg', simp add: mult.commute) []
   449         apply (insert Mg'', simp) []
   450         apply (simp split: split_indicator add: derivg_nonneg)
   451         apply (rule notinf)
   452         apply (simp split: split_indicator add: derivg_nonneg)
   453         done
   454       also have "... = \<integral>\<^sup>+ x. indicator (-A) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
   455         by (intro nn_integral_cong) (simp split: split_indicator)
   456       finally show ?case .
   457 
   458     next
   459       case (union f)
   460       then have [simp]: "\<And>i. {a..b} \<inter> g -` f i \<in> sets borel"
   461         by (subst Int_commute, intro set_borel_measurable_sets[OF Mg]) auto
   462       have "g -` (\<Union>i. f i) \<inter> {a..b} = (\<Union>i. {a..b} \<inter> g -` f i)" by auto
   463       hence "g -` (\<Union>i. f i) \<inter> {a..b} \<in> sets borel" by (auto simp del: UN_simps)
   464 
   465       have "(\<integral>\<^sup>+x. indicator (\<Union>i. f i) x * indicator {g a..g b} x \<partial>lborel) = 
   466                 \<integral>\<^sup>+x. indicator (\<Union>i. {g a..g b} \<inter> f i) x \<partial>lborel"
   467           by (intro nn_integral_cong) (simp split: split_indicator)
   468       also from union have "... = emeasure lborel (\<Union>i. {g a..g b} \<inter> f i)" by simp
   469       also from union have "... = (\<Sum>i. emeasure lborel ({g a..g b} \<inter> f i))"
   470         by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def)
   471       also from union have "... = (\<Sum>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel)" by simp
   472       also have "(\<lambda>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel) = 
   473                            (\<lambda>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel)"
   474         by (intro ext nn_integral_cong) (simp split: split_indicator)
   475       also from union.IH have "(\<Sum>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel) = 
   476           (\<Sum>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)" by simp
   477       also have "(\<lambda>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) =
   478                          (\<lambda>i. \<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x \<partial>lborel)"
   479         by (intro ext nn_integral_cong) (simp split: split_indicator)
   480       also have "(\<Sum>i. ... i) = \<integral>\<^sup>+ x. (\<Sum>i. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) \<partial>lborel"
   481         using Mg'
   482         apply (intro nn_integral_suminf[symmetric])
   483         apply (rule borel_measurable_ereal_times, simp add: borel_measurable_ereal mult.commute)
   484         apply (rule borel_measurable_indicator, subst sets_lborel)
   485         apply (simp_all split: split_indicator add: derivg_nonneg)
   486         done
   487       also have "(\<lambda>x i. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) =
   488                       (\<lambda>x i. ereal (g' x * indicator {a..b} x) * indicator (g -` f i) x)"
   489         by (intro ext) (simp split: split_indicator)
   490       also have "(\<integral>\<^sup>+ x. (\<Sum>i. ereal (g' x * indicator {a..b} x) * indicator (g -` f i) x) \<partial>lborel) =
   491                      \<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) * (\<Sum>i. indicator (g -` f i) x) \<partial>lborel"
   492         by (intro nn_integral_cong suminf_cmult_ereal) (auto split: split_indicator simp: derivg_nonneg)
   493       also from union have "(\<lambda>x. \<Sum>i. indicator (g -` f i) x :: ereal) = (\<lambda>x. indicator (\<Union>i. g -` f i) x)"
   494         by (intro ext suminf_indicator) (auto simp: disjoint_family_on_def)
   495       also have "(\<integral>\<^sup>+x. ereal (g' x * indicator {a..b} x) * ... x \<partial>lborel) =
   496                     (\<integral>\<^sup>+x. indicator (\<Union>i. f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
   497        by (intro nn_integral_cong) (simp split: split_indicator)
   498       finally show ?case .
   499   qed
   500 
   501 next
   502   case (mult f c)
   503     note Mf[measurable] = `f \<in> borel_measurable borel`
   504     let ?I = "indicator {a..b}"
   505     have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
   506       by (intro borel_measurable_ereal_times measurable_compose[OF _ Mf])
   507          (simp_all add: borel_measurable_ereal mult.commute)
   508     also have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. f (g x) * ereal (g' x) * ?I x)"
   509       by (intro ext) (simp split: split_indicator)
   510     finally have Mf': "(\<lambda>x. f (g x) * ereal (g' x) * ?I x) \<in> borel_measurable borel" .
   511     with mult show ?case
   512       by (subst (1 2 3) mult_ac, subst (1 2) nn_integral_cmult) (simp_all add: mult_ac)
   513  
   514 next
   515   case (add f2 f1)
   516     let ?I = "indicator {a..b}"
   517     {
   518       fix f :: "real \<Rightarrow> ereal" assume Mf: "f \<in> borel_measurable borel"
   519       have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
   520         by (intro borel_measurable_ereal_times measurable_compose[OF _ Mf])
   521            (simp_all add: borel_measurable_ereal mult.commute)
   522       also have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. f (g x) * ereal (g' x) * ?I x)"
   523         by (intro ext) (simp split: split_indicator)
   524       finally have "(\<lambda>x. f (g x) * ereal (g' x) * ?I x) \<in> borel_measurable borel" .
   525     } note Mf' = this[OF `f1 \<in> borel_measurable borel`] this[OF `f2 \<in> borel_measurable borel`]
   526     from add have not_neginf: "\<And>x. f1 x \<noteq> -\<infinity>" "\<And>x. f2 x \<noteq> -\<infinity>" 
   527       by (metis Infty_neq_0(1) ereal_0_le_uminus_iff ereal_infty_less_eq(1))+
   528 
   529     have "(\<integral>\<^sup>+ x. (f1 x + f2 x) * indicator {g a..g b} x \<partial>lborel) =
   530              (\<integral>\<^sup>+ x. f1 x * indicator {g a..g b} x + f2 x * indicator {g a..g b} x \<partial>lborel)"
   531       by (intro nn_integral_cong) (simp split: split_indicator)
   532     also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) +
   533                                 (\<integral>\<^sup>+ x. f2 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
   534       by (simp_all add: nn_integral_add)
   535     also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ereal (g' x) * indicator {a..b} x + 
   536                                       f2 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
   537       by (intro nn_integral_add[symmetric])
   538          (auto simp add: Mf' derivg_nonneg split: split_indicator)
   539     also from not_neginf have "... = \<integral>\<^sup>+ x. (f1 (g x) + f2 (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
   540       by (intro nn_integral_cong) (simp split: split_indicator add: ereal_distrib)
   541     finally show ?case .
   542 
   543 next
   544   case (sup F)
   545   {
   546     fix i
   547     let ?I = "indicator {a..b}"
   548     have "(\<lambda>x. F i (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
   549       by (rule_tac borel_measurable_ereal_times, rule_tac measurable_compose[OF _ sup.hyps(1)])
   550          (simp_all add: mult.commute)
   551     also have "(\<lambda>x. F i (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. F i (g x) * ereal (g' x) * ?I x)"
   552       by (intro ext) (simp split: split_indicator)
   553      finally have "... \<in> borel_measurable borel" .
   554   } note Mf' = this
   555 
   556     have "(\<integral>\<^sup>+x. (SUP i. F i x) * indicator {g a..g b} x \<partial>lborel) = 
   557                \<integral>\<^sup>+x. (SUP i. F i x* indicator {g a..g b} x) \<partial>lborel"
   558       by (intro nn_integral_cong) (simp split: split_indicator)
   559     also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i x* indicator {g a..g b} x \<partial>lborel)"
   560       by (intro nn_integral_monotone_convergence_SUP)
   561          (auto simp: incseq_def le_fun_def split: split_indicator)
   562     also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
   563       by simp
   564     also from sup have "... =  \<integral>\<^sup>+x. (SUP i. F i (g x) * ereal (g' x) * indicator {a..b} x) \<partial>lborel"
   565       by (intro nn_integral_monotone_convergence_SUP[symmetric])
   566          (auto simp: incseq_def le_fun_def derivg_nonneg Mf' split: split_indicator
   567                intro!: ereal_mult_right_mono)
   568     also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
   569       by (subst mult.assoc, subst mult.commute, subst SUP_ereal_cmult)
   570          (auto split: split_indicator simp: derivg_nonneg mult_ac)
   571     finally show ?case by simp
   572   qed
   573 qed
   574 
   575 lemma nn_integral_substitution:
   576   fixes f :: "real \<Rightarrow> real"
   577   assumes Mf[measurable]: "set_borel_measurable borel {g a..g b} f"
   578   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   579   assumes contg': "continuous_on {a..b} g'" 
   580   assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   581   assumes "a \<le> b"
   582   shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
   583              (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
   584 proof (cases "a = b")
   585   assume "a \<noteq> b"
   586   with `a \<le> b` have "a < b" by auto
   587   let ?f' = "\<lambda>x. max 0 (f x * indicator {g a..g b} x)"
   588 
   589   from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
   590     by (rule deriv_nonneg_imp_mono) simp_all
   591   have bounds: "\<And>x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g x \<ge> g a" "\<And>x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g x \<le> g b"
   592     by (auto intro: monog)
   593 
   594   from derivg_nonneg have nonneg: 
   595     "\<And>f x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g' x \<noteq> 0 \<Longrightarrow> f x * ereal (g' x) \<ge> 0 \<Longrightarrow> f x \<ge> 0"
   596     by (force simp: ereal_zero_le_0_iff field_simps)
   597   have nonneg': "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<not> 0 \<le> f (g x) \<Longrightarrow> 0 \<le> f (g x) * g' x \<Longrightarrow> g' x = 0"
   598     by (metis atLeastAtMost_iff derivg_nonneg eq_iff mult_eq_0_iff mult_le_0_iff)
   599 
   600   have "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
   601             (\<integral>\<^sup>+x. ereal (?f' x) * indicator {g a..g b} x \<partial>lborel)"
   602     by (subst nn_integral_max_0[symmetric], intro nn_integral_cong) 
   603        (auto split: split_indicator simp: zero_ereal_def)
   604   also have "... = \<integral>\<^sup>+ x. ?f' (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel" using Mf
   605     by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg `a < b`]) 
   606        (auto simp add: zero_ereal_def mult.commute)
   607   also have "... = \<integral>\<^sup>+ x. max 0 (f (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
   608     by (intro nn_integral_cong) 
   609        (auto split: split_indicator simp: max_def dest: bounds)
   610   also have "... = \<integral>\<^sup>+ x. max 0 (f (g x) * ereal (g' x) * indicator {a..b} x) \<partial>lborel"
   611     by (intro nn_integral_cong)
   612        (auto simp: max_def derivg_nonneg split: split_indicator intro!: nonneg')
   613   also have "... = \<integral>\<^sup>+ x. f (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
   614     by (rule nn_integral_max_0)
   615   also have "... = \<integral>\<^sup>+x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel"
   616     by (intro nn_integral_cong) (simp split: split_indicator)
   617   finally show ?thesis .
   618 qed auto
   619 
   620 lemma integral_substitution:
   621   assumes integrable: "set_integrable lborel {g a..g b} f"
   622   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   623   assumes contg': "continuous_on {a..b} g'" 
   624   assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   625   assumes "a \<le> b"
   626   shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
   627     and "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)"
   628 proof-
   629   from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
   630   from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and 
   631                              Mg': "set_borel_measurable borel {a..b} g'" 
   632       by (simp_all only: set_measurable_continuous_on_ivl)
   633   from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
   634     by (rule deriv_nonneg_imp_mono) simp_all
   635 
   636   have "(\<lambda>x. ereal (f x) * indicator {g a..g b} x) = 
   637            (\<lambda>x. ereal (f x * indicator {g a..g b} x))" 
   638     by (intro ext) (simp split: split_indicator)
   639   with integrable have M1: "(\<lambda>x. f x * indicator {g a..g b} x) \<in> borel_measurable borel"
   640     unfolding real_integrable_def by (force simp: mult.commute)
   641   have "(\<lambda>x. ereal (-f x) * indicator {g a..g b} x) = 
   642            (\<lambda>x. -ereal (f x * indicator {g a..g b} x))" 
   643     by (intro ext) (simp split: split_indicator)
   644   with integrable have M2: "(\<lambda>x. -f x * indicator {g a..g b} x) \<in> borel_measurable borel"
   645     unfolding real_integrable_def by (force simp: mult.commute)
   646 
   647   have "LBINT x. (f x :: real) * indicator {g a..g b} x = 
   648           real (\<integral>\<^sup>+ x. ereal (f x) * indicator {g a..g b} x \<partial>lborel) -
   649           real (\<integral>\<^sup>+ x. ereal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
   650     by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ereal mult.commute)
   651   also have "(\<integral>\<^sup>+x. ereal (f x) * indicator {g a..g b} x \<partial>lborel) =
   652                (\<integral>\<^sup>+x. ereal (f x * indicator {g a..g b} x) \<partial>lborel)"
   653     by (intro nn_integral_cong) (simp split: split_indicator)
   654   also with M1 have A: "(\<integral>\<^sup>+ x. ereal (f x * indicator {g a..g b} x) \<partial>lborel) =
   655                             (\<integral>\<^sup>+ x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)"
   656     by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg `a \<le> b`]) 
   657        (auto simp: nn_integral_set_ereal mult.commute)
   658   also have "(\<integral>\<^sup>+ x. ereal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
   659                (\<integral>\<^sup>+ x. ereal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
   660     by (intro nn_integral_cong) (simp split: split_indicator)
   661   also with M2 have B: "(\<integral>\<^sup>+ x. ereal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
   662                             (\<integral>\<^sup>+ x. ereal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
   663     by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg `a \<le> b`])
   664        (auto simp: nn_integral_set_ereal mult.commute)
   665 
   666   also {
   667     from integrable have Mf: "set_borel_measurable borel {g a..g b} f" 
   668       unfolding real_integrable_def by simp
   669     from borel_measurable_times[OF measurable_compose[OF Mg Mf] Mg']
   670       have "(\<lambda>x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
   671                      (g' x * indicator {a..b} x)) \<in> borel_measurable borel"  (is "?f \<in> _") 
   672       by (simp add: mult.commute)
   673     also have "?f = (\<lambda>x. f (g x) * g' x * indicator {a..b} x)"
   674       using monog by (intro ext) (auto split: split_indicator)
   675     finally show "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
   676       using A B integrable unfolding real_integrable_def 
   677       by (simp_all add: nn_integral_set_ereal mult.commute)
   678   } note integrable' = this
   679 
   680   have "real (\<integral>\<^sup>+ x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel) -
   681                   real (\<integral>\<^sup>+ x. ereal (-f (g x) * g' x * indicator {a..b} x) \<partial>lborel) =
   682                 (LBINT x. f (g x) * g' x * indicator {a..b} x)" using integrable'
   683     by (subst real_lebesgue_integral_def) (simp_all add: field_simps)
   684   finally show "(LBINT x. f x * indicator {g a..g b} x) = 
   685                      (LBINT x. f (g x) * g' x * indicator {a..b} x)" .
   686 qed
   687 
   688 lemma interval_integral_substitution:
   689   assumes integrable: "set_integrable lborel {g a..g b} f"
   690   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   691   assumes contg': "continuous_on {a..b} g'" 
   692   assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   693   assumes "a \<le> b"
   694   shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
   695     and "(LBINT x=g a..g b. f x) = (LBINT x=a..b. f (g x) * g' x)"
   696   apply (rule integral_substitution[OF assms], simp, simp)
   697   apply (subst (1 2) interval_integral_Icc, fact)
   698   apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact)
   699   using integral_substitution(2)[OF assms]
   700   apply (simp add: mult.commute)
   701   done
   702 
   703 lemma set_borel_integrable_singleton[simp]:
   704   "set_integrable lborel {x} (f :: real \<Rightarrow> real)"
   705   by (subst integrable_discrete_difference[where X="{x}" and g="\<lambda>_. 0"]) auto
   706 
   707 end