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