src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago)
changeset 69981 3dced198b9ec
parent 69861 62e47f06d22c
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:      HOL/Analysis/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 \<open>Integration by Substition for the Lebesgue Integral\<close>
    10 
    11 theory Lebesgue_Integral_Substitution
    12 imports Interval_Integral
    13 begin
    14 
    15 
    16 lemma nn_integral_substitution_aux:
    17   fixes f :: "real \<Rightarrow> ennreal"
    18   assumes Mf: "f \<in> borel_measurable borel"
    19   assumes nonnegf: "\<And>x. f x \<ge> 0"
    20   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
    21   assumes contg': "continuous_on {a..b} g'"
    22   assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
    23   assumes "a < b"
    24   shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) =
    25              (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
    26 proof-
    27   from \<open>a < b\<close> have [simp]: "a \<le> b" by simp
    28   from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
    29   from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and
    30                              Mg': "set_borel_measurable borel {a..b} g'"
    31       by (simp_all only: set_measurable_continuous_on_ivl)
    32   from derivg have derivg': "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
    33     by (simp only: has_field_derivative_iff_has_vector_derivative)
    34 
    35   have real_ind[simp]: "\<And>A x. enn2real (indicator A x) = indicator A x"
    36       by (auto split: split_indicator)
    37   have ennreal_ind[simp]: "\<And>A x. ennreal (indicator A x) = indicator A x"
    38       by (auto split: split_indicator)
    39   have [simp]: "\<And>x A. indicator A (g x) = indicator (g -` A) x"
    40       by (auto split: split_indicator)
    41 
    42   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"
    43     by (rule deriv_nonneg_imp_mono) simp_all
    44   with monog have [simp]: "g a \<le> g b" by (auto intro: mono_onD)
    45 
    46   show ?thesis
    47   proof (induction rule: borel_measurable_induct[OF Mf, case_names cong set mult add sup])
    48     case (cong f1 f2)
    49     from cong.hyps(3) have "f1 = f2" by auto
    50     with cong show ?case by simp
    51   next
    52     case (set A)
    53     from set.hyps show ?case
    54     proof (induction rule: borel_set_induct)
    55       case empty
    56       thus ?case by simp
    57     next
    58       case (interval c d)
    59       {
    60         fix u v :: real assume asm: "{u..v} \<subseteq> {g a..g b}" "u \<le> v"
    61 
    62         obtain u' v' where u'v': "{a..b} \<inter> g-`{u..v} = {u'..v'}" "u' \<le> v'" "g u' = u" "g v' = v"
    63              using asm by (rule_tac continuous_interval_vimage_Int[OF contg monog, of u v]) simp_all
    64         hence "{u'..v'} \<subseteq> {a..b}" "{u'..v'} \<subseteq> g -` {u..v}" by blast+
    65         with u'v'(2) have "u' \<in> g -` {u..v}" "v' \<in> g -` {u..v}" by auto
    66         from u'v'(1) have [simp]: "{a..b} \<inter> g -` {u..v} \<in> sets borel" by simp
    67 
    68         have A: "continuous_on {min u' v'..max u' v'} g'"
    69             by (simp only: u'v' max_absorb2 min_absorb1)
    70                (intro continuous_on_subset[OF contg'], insert u'v', auto)
    71         have "\<And>x. x \<in> {u'..v'} \<Longrightarrow> (g has_real_derivative g' x) (at x within {u'..v'})"
    72            using asm by (intro has_field_derivative_subset[OF derivg] subsetD[OF \<open>{u'..v'} \<subseteq> {a..b}\<close>]) auto
    73         hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow>
    74                       (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})"
    75             by (simp only: u'v' max_absorb2 min_absorb1)
    76                (auto simp: has_field_derivative_iff_has_vector_derivative)
    77           have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
    78             using set_integrable_subset borel_integrable_atLeastAtMost'[OF contg']
    79             by (metis \<open>{u'..v'} \<subseteq> {a..b}\<close> eucl_ivals(5) set_integrable_def sets_lborel u'v'(1))
    80         hence "(\<integral>\<^sup>+x. ennreal (g' x) * indicator ({a..b} \<inter> g-` {u..v}) x \<partial>lborel) =
    81                    LBINT x:{a..b} \<inter> g-`{u..v}. g' x"
    82           unfolding set_lebesgue_integral_def
    83           by (subst nn_integral_eq_integral[symmetric])
    84              (auto intro!: derivg_nonneg nn_integral_cong split: split_indicator)
    85         also from interval_integral_FTC_finite[OF A B]
    86             have "LBINT x:{a..b} \<inter> g-`{u..v}. g' x = v - u"
    87                 by (simp add: u'v' interval_integral_Icc \<open>u \<le> v\<close>)
    88         finally have "(\<integral>\<^sup>+ x. ennreal (g' x) * indicator ({a..b} \<inter> g -` {u..v}) x \<partial>lborel) =
    89                            ennreal (v - u)" .
    90       } note A = this
    91 
    92       have "(\<integral>\<^sup>+x. indicator {c..d} (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel) =
    93                (\<integral>\<^sup>+ x. ennreal (g' x) * indicator ({a..b} \<inter> g -` {c..d}) x \<partial>lborel)"
    94         by (intro nn_integral_cong) (simp split: split_indicator)
    95       also have "{a..b} \<inter> g-`{c..d} = {a..b} \<inter> g-`{max (g a) c..min (g b) d}"
    96         using \<open>a \<le> b\<close> \<open>c \<le> d\<close>
    97         by (auto intro!: monog intro: order.trans)
    98       also have "(\<integral>\<^sup>+ x. ennreal (g' x) * indicator ... x \<partial>lborel) =
    99         (if max (g a) c \<le> min (g b) d then min (g b) d - max (g a) c else 0)"
   100          using \<open>c \<le> d\<close> by (simp add: A)
   101       also have "... = (\<integral>\<^sup>+ x. indicator ({g a..g b} \<inter> {c..d}) x \<partial>lborel)"
   102         by (subst nn_integral_indicator) (auto intro!: measurable_sets Mg simp:)
   103       also have "... = (\<integral>\<^sup>+ x. indicator {c..d} x * indicator {g a..g b} x \<partial>lborel)"
   104         by (intro nn_integral_cong) (auto split: split_indicator)
   105       finally show ?case ..
   106 
   107       next
   108 
   109       case (compl A)
   110       note \<open>A \<in> sets borel\<close>[measurable]
   111       from emeasure_mono[of "A \<inter> {g a..g b}" "{g a..g b}" lborel]
   112       have [simp]: "emeasure lborel (A \<inter> {g a..g b}) \<noteq> top" by (auto simp: top_unique)
   113       have [simp]: "g -` A \<inter> {a..b} \<in> sets borel"
   114         by (rule set_borel_measurable_sets[OF Mg]) auto
   115       have [simp]: "g -` (-A) \<inter> {a..b} \<in> sets borel"
   116         by (rule set_borel_measurable_sets[OF Mg]) auto
   117 
   118       have "(\<integral>\<^sup>+x. indicator (-A) x * indicator {g a..g b} x \<partial>lborel) =
   119                 (\<integral>\<^sup>+x. indicator (-A \<inter> {g a..g b}) x \<partial>lborel)"
   120         by (rule nn_integral_cong) (simp split: split_indicator)
   121       also from compl have "... = emeasure lborel ({g a..g b} - A)" using derivg_nonneg
   122         by (simp add: vimage_Compl diff_eq Int_commute[of "-A"])
   123       also have "{g a..g b} - A = {g a..g b} - A \<inter> {g a..g b}" by blast
   124       also have "emeasure lborel ... = g b - g a - emeasure lborel (A \<inter> {g a..g b})"
   125              using \<open>A \<in> sets borel\<close> by (subst emeasure_Diff) (auto simp: )
   126      also have "emeasure lborel (A \<inter> {g a..g b}) =
   127                     \<integral>\<^sup>+x. indicator A x * indicator {g a..g b} x \<partial>lborel"
   128        using \<open>A \<in> sets borel\<close>
   129        by (subst nn_integral_indicator[symmetric], simp, intro nn_integral_cong)
   130           (simp split: split_indicator)
   131       also have "... = \<integral>\<^sup>+ x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel" (is "_ = ?I")
   132         by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator)
   133       also have "g b - g a = LBINT x:{a..b}. g' x" using derivg'
   134         unfolding set_lebesgue_integral_def
   135         by (intro integral_FTC_atLeastAtMost[symmetric])
   136            (auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg]
   137                  has_vector_derivative_at_within)
   138       also have "ennreal ... = \<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel"
   139         using borel_integrable_atLeastAtMost'[OF contg'] unfolding set_lebesgue_integral_def
   140         by (subst nn_integral_eq_integral)
   141            (simp_all add: mult.commute derivg_nonneg set_integrable_def split: split_indicator)
   142       also have Mg'': "(\<lambda>x. indicator (g -` A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x))
   143                             \<in> borel_measurable borel" using Mg'
   144         by (intro borel_measurable_times_ennreal borel_measurable_indicator)
   145            (simp_all add: mult.commute set_borel_measurable_def)
   146       have le: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel) \<le>
   147                         (\<integral>\<^sup>+x. ennreal (g' x) * indicator {a..b} x \<partial>lborel)"
   148          by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg)
   149       note integrable = borel_integrable_atLeastAtMost'[OF contg']
   150       with le have notinf: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel) \<noteq> top"
   151           by (auto simp: real_integrable_def nn_integral_set_ennreal mult.commute top_unique set_integrable_def)
   152       have "(\<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel) - ?I =
   153                   \<integral>\<^sup>+ x. ennreal (g' x * indicator {a..b} x) -
   154                         indicator (g -` A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel"
   155         apply (intro nn_integral_diff[symmetric])
   156         apply (insert Mg', simp add: mult.commute set_borel_measurable_def) []
   157         apply (insert Mg'', simp) []
   158         apply (simp split: split_indicator add: derivg_nonneg)
   159         apply (rule notinf)
   160         apply (simp split: split_indicator add: derivg_nonneg)
   161         done
   162       also have "... = \<integral>\<^sup>+ x. indicator (-A) (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel"
   163         by (intro nn_integral_cong) (simp split: split_indicator)
   164       finally show ?case .
   165 
   166     next
   167       case (union f)
   168       then have [simp]: "\<And>i. {a..b} \<inter> g -` f i \<in> sets borel"
   169         by (subst Int_commute, intro set_borel_measurable_sets[OF Mg]) auto
   170       have "g -` (\<Union>i. f i) \<inter> {a..b} = (\<Union>i. {a..b} \<inter> g -` f i)" by auto
   171       hence "g -` (\<Union>i. f i) \<inter> {a..b} \<in> sets borel" by (auto simp del: UN_simps)
   172 
   173       have "(\<integral>\<^sup>+x. indicator (\<Union>i. f i) x * indicator {g a..g b} x \<partial>lborel) =
   174                 \<integral>\<^sup>+x. indicator (\<Union>i. {g a..g b} \<inter> f i) x \<partial>lborel"
   175           by (intro nn_integral_cong) (simp split: split_indicator)
   176       also from union have "... = emeasure lborel (\<Union>i. {g a..g b} \<inter> f i)" by simp
   177       also from union have "... = (\<Sum>i. emeasure lborel ({g a..g b} \<inter> f i))"
   178         by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def)
   179       also from union have "... = (\<Sum>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel)" by simp
   180       also have "(\<lambda>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel) =
   181                            (\<lambda>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel)"
   182         by (intro ext nn_integral_cong) (simp split: split_indicator)
   183       also from union.IH have "(\<Sum>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel) =
   184           (\<Sum>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel)" by simp
   185       also have "(\<lambda>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel) =
   186                          (\<lambda>i. \<integral>\<^sup>+ x. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x \<partial>lborel)"
   187         by (intro ext nn_integral_cong) (simp split: split_indicator)
   188       also have "(\<Sum>i. ... i) = \<integral>\<^sup>+ x. (\<Sum>i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) \<partial>lborel"
   189         using Mg'
   190         apply (intro nn_integral_suminf[symmetric])
   191         apply (rule borel_measurable_times_ennreal, simp add: mult.commute set_borel_measurable_def)
   192         apply (rule borel_measurable_indicator, subst sets_lborel)
   193         apply (simp_all split: split_indicator add: derivg_nonneg)
   194         done
   195       also have "(\<lambda>x i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) =
   196                       (\<lambda>x i. ennreal (g' x * indicator {a..b} x) * indicator (g -` f i) x)"
   197         by (intro ext) (simp split: split_indicator)
   198       also have "(\<integral>\<^sup>+ x. (\<Sum>i. ennreal (g' x * indicator {a..b} x) * indicator (g -` f i) x) \<partial>lborel) =
   199                      \<integral>\<^sup>+ x. ennreal (g' x * indicator {a..b} x) * (\<Sum>i. indicator (g -` f i) x) \<partial>lborel"
   200         by (intro nn_integral_cong) (auto split: split_indicator simp: derivg_nonneg)
   201       also from union have "(\<lambda>x. \<Sum>i. indicator (g -` f i) x :: ennreal) = (\<lambda>x. indicator (\<Union>i. g -` f i) x)"
   202         by (intro ext suminf_indicator) (auto simp: disjoint_family_on_def)
   203       also have "(\<integral>\<^sup>+x. ennreal (g' x * indicator {a..b} x) * ... x \<partial>lborel) =
   204                     (\<integral>\<^sup>+x. indicator (\<Union>i. f i) (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel)"
   205        by (intro nn_integral_cong) (simp split: split_indicator)
   206       finally show ?case .
   207   qed
   208 
   209 next
   210   case (mult f c)
   211     note Mf[measurable] = \<open>f \<in> borel_measurable borel\<close>
   212     let ?I = "indicator {a..b}"
   213     have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
   214       by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
   215          (simp_all add: mult.commute set_borel_measurable_def)
   216     also have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. f (g x) * ennreal (g' x) * ?I x)"
   217       by (intro ext) (simp split: split_indicator)
   218     finally have Mf': "(\<lambda>x. f (g x) * ennreal (g' x) * ?I x) \<in> borel_measurable borel" .
   219     with mult show ?case
   220       by (subst (1 2 3) mult_ac, subst (1 2) nn_integral_cmult) (simp_all add: mult_ac)
   221 
   222 next
   223   case (add f2 f1)
   224     let ?I = "indicator {a..b}"
   225     {
   226       fix f :: "real \<Rightarrow> ennreal" assume Mf: "f \<in> borel_measurable borel"
   227       have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
   228         by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
   229            (simp_all add:  mult.commute set_borel_measurable_def)
   230       also have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. f (g x) * ennreal (g' x) * ?I x)"
   231         by (intro ext) (simp split: split_indicator)
   232       finally have "(\<lambda>x. f (g x) * ennreal (g' x) * ?I x) \<in> borel_measurable borel" .
   233     } note Mf' = this[OF \<open>f1 \<in> borel_measurable borel\<close>] this[OF \<open>f2 \<in> borel_measurable borel\<close>]
   234 
   235     have "(\<integral>\<^sup>+ x. (f1 x + f2 x) * indicator {g a..g b} x \<partial>lborel) =
   236              (\<integral>\<^sup>+ x. f1 x * indicator {g a..g b} x + f2 x * indicator {g a..g b} x \<partial>lborel)"
   237       by (intro nn_integral_cong) (simp split: split_indicator)
   238     also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel) +
   239                                 (\<integral>\<^sup>+ x. f2 (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel)"
   240       by (simp_all add: nn_integral_add)
   241     also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ennreal (g' x) * indicator {a..b} x +
   242                                       f2 (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel)"
   243       by (intro nn_integral_add[symmetric])
   244          (auto simp add: Mf' derivg_nonneg split: split_indicator)
   245     also have "... = \<integral>\<^sup>+ x. (f1 (g x) + f2 (g x)) * ennreal (g' x) * indicator {a..b} x \<partial>lborel"
   246       by (intro nn_integral_cong) (simp split: split_indicator add: distrib_right)
   247     finally show ?case .
   248 
   249 next
   250   case (sup F)
   251   {
   252     fix i
   253     let ?I = "indicator {a..b}"
   254     have "(\<lambda>x. F i (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
   255       by (rule_tac borel_measurable_times_ennreal, rule_tac measurable_compose[OF _ sup.hyps(1)])
   256          (simp_all add: mult.commute set_borel_measurable_def)
   257     also have "(\<lambda>x. F i (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. F i (g x) * ennreal (g' x) * ?I x)"
   258       by (intro ext) (simp split: split_indicator)
   259      finally have "... \<in> borel_measurable borel" .
   260   } note Mf' = this
   261 
   262     have "(\<integral>\<^sup>+x. (SUP i. F i x) * indicator {g a..g b} x \<partial>lborel) =
   263                \<integral>\<^sup>+x. (SUP i. F i x* indicator {g a..g b} x) \<partial>lborel"
   264       by (intro nn_integral_cong) (simp split: split_indicator)
   265     also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i x* indicator {g a..g b} x \<partial>lborel)"
   266       by (intro nn_integral_monotone_convergence_SUP)
   267          (auto simp: incseq_def le_fun_def split: split_indicator)
   268     also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel)"
   269       by simp
   270     also from sup have "... =  \<integral>\<^sup>+x. (SUP i. F i (g x) * ennreal (g' x) * indicator {a..b} x) \<partial>lborel"
   271       by (intro nn_integral_monotone_convergence_SUP[symmetric])
   272          (auto simp: incseq_def le_fun_def derivg_nonneg Mf' split: split_indicator
   273                intro!: mult_right_mono)
   274     also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x)) * ennreal (g' x) * indicator {a..b} x \<partial>lborel"
   275       by (subst mult.assoc, subst mult.commute, subst SUP_mult_left_ennreal)
   276          (auto split: split_indicator simp: derivg_nonneg mult_ac)
   277     finally show ?case by (simp add: image_comp)
   278   qed
   279 qed
   280 
   281 theorem nn_integral_substitution:
   282   fixes f :: "real \<Rightarrow> real"
   283   assumes Mf[measurable]: "set_borel_measurable borel {g a..g b} f"
   284   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   285   assumes contg': "continuous_on {a..b} g'"
   286   assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   287   assumes "a \<le> b"
   288   shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) =
   289              (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
   290 proof (cases "a = b")
   291   assume "a \<noteq> b"
   292   with \<open>a \<le> b\<close> have "a < b" by auto
   293   let ?f' = "\<lambda>x. f x * indicator {g a..g b} x"
   294 
   295   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"
   296     by (rule deriv_nonneg_imp_mono) simp_all
   297   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"
   298     by (auto intro: monog)
   299 
   300   from derivg_nonneg have nonneg:
   301     "\<And>f x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g' x \<noteq> 0 \<Longrightarrow> f x * ennreal (g' x) \<ge> 0 \<Longrightarrow> f x \<ge> 0"
   302     by (force simp: field_simps)
   303   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"
   304     by (metis atLeastAtMost_iff derivg_nonneg eq_iff mult_eq_0_iff mult_le_0_iff)
   305 
   306   have "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) =
   307             (\<integral>\<^sup>+x. ennreal (?f' x) * indicator {g a..g b} x \<partial>lborel)"
   308     by (intro nn_integral_cong)
   309        (auto split: split_indicator split_max simp: zero_ennreal.rep_eq ennreal_neg)
   310   also have "... = \<integral>\<^sup>+ x. ?f' (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel" using Mf
   311     by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg \<open>a < b\<close>])
   312        (auto simp add: mult.commute set_borel_measurable_def)
   313   also have "... = \<integral>\<^sup>+ x. f (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel"
   314     by (intro nn_integral_cong) (auto split: split_indicator simp: max_def dest: bounds)
   315   also have "... = \<integral>\<^sup>+x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel"
   316     by (intro nn_integral_cong) (auto simp: mult.commute derivg_nonneg ennreal_mult' split: split_indicator)
   317   finally show ?thesis .
   318 qed auto
   319 
   320 theorem integral_substitution:
   321   assumes integrable: "set_integrable lborel {g a..g b} f"
   322   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   323   assumes contg': "continuous_on {a..b} g'"
   324   assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   325   assumes "a \<le> b"
   326   shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
   327     and "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)"
   328 proof-
   329   from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
   330   with contg' have Mg: "set_borel_measurable borel {a..b} g"
   331     and Mg': "set_borel_measurable borel {a..b} g'"
   332     by (simp_all only: set_measurable_continuous_on_ivl)
   333   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"
   334     by (rule deriv_nonneg_imp_mono) simp_all
   335 
   336   have "(\<lambda>x. ennreal (f x) * indicator {g a..g b} x) =
   337            (\<lambda>x. ennreal (f x * indicator {g a..g b} x))"
   338     by (intro ext) (simp split: split_indicator)
   339   with integrable have M1: "(\<lambda>x. f x * indicator {g a..g b} x) \<in> borel_measurable borel"
   340     by (force simp: mult.commute set_integrable_def)
   341   from integrable have M2: "(\<lambda>x. -f x * indicator {g a..g b} x) \<in> borel_measurable borel"
   342     by (force simp: mult.commute set_integrable_def)
   343 
   344   have "LBINT x. (f x :: real) * indicator {g a..g b} x =
   345           enn2real (\<integral>\<^sup>+ x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) -
   346           enn2real (\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
   347     unfolding set_integrable_def
   348     by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ennreal mult.commute)
   349   also have *: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) =
   350       (\<integral>\<^sup>+x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel)"
   351     by (intro nn_integral_cong) (simp split: split_indicator)
   352   also from M1 * have A: "(\<integral>\<^sup>+ x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel) =
   353                             (\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)"
   354     by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
   355        (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)
   356   also have **: "(\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
   357       (\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
   358     by (intro nn_integral_cong) (simp split: split_indicator)
   359   also from M2 ** have B: "(\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
   360         (\<integral>\<^sup>+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
   361     by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
   362        (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)
   363 
   364   also {
   365     from integrable have Mf: "set_borel_measurable borel {g a..g b} f"
   366       unfolding set_borel_measurable_def set_integrable_def by simp
   367     from measurable_compose Mg Mf Mg' borel_measurable_times
   368     have "(\<lambda>x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
   369                      (g' x * indicator {a..b} x)) \<in> borel_measurable borel"  (is "?f \<in> _")
   370       by (simp add: mult.commute set_borel_measurable_def)
   371     also have "?f = (\<lambda>x. f (g x) * g' x * indicator {a..b} x)"
   372       using monog by (intro ext) (auto split: split_indicator)
   373     finally show "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
   374       using A B integrable unfolding real_integrable_def set_integrable_def
   375       by (simp_all add: nn_integral_set_ennreal mult.commute)
   376   } note integrable' = this
   377 
   378   have "enn2real (\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel) -
   379                   enn2real (\<integral>\<^sup>+ x. ennreal (-f (g x) * g' x * indicator {a..b} x) \<partial>lborel) =
   380                 (LBINT x. f (g x) * g' x * indicator {a..b} x)" 
   381     using integrable' unfolding set_integrable_def
   382     by (subst real_lebesgue_integral_def) (simp_all add: field_simps)
   383   finally show "(LBINT x. f x * indicator {g a..g b} x) =
   384                      (LBINT x. f (g x) * g' x * indicator {a..b} x)" .
   385 qed
   386 
   387 theorem interval_integral_substitution:
   388   assumes integrable: "set_integrable lborel {g a..g b} f"
   389   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   390   assumes contg': "continuous_on {a..b} g'"
   391   assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   392   assumes "a \<le> b"
   393   shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
   394     and "(LBINT x=g a..g b. f x) = (LBINT x=a..b. f (g x) * g' x)"
   395   apply (rule integral_substitution[OF assms], simp, simp)
   396   apply (subst (1 2) interval_integral_Icc, fact)
   397   apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact)
   398   using integral_substitution(2)[OF assms]
   399   apply (simp add: mult.commute set_lebesgue_integral_def)
   400   done
   401 
   402 lemma set_borel_integrable_singleton[simp]: "set_integrable lborel {x} (f :: real \<Rightarrow> real)"
   403   unfolding set_integrable_def
   404   by (subst integrable_discrete_difference[where X="{x}" and g="\<lambda>_. 0"]) auto
   405 
   406 end