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
```