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